Chun Tian

Furthermore, I found that the existing `Sub_and_cond.COND_ELIM_CONV` has some knowledge on integer arithmetics, and it can also do `ABS_CONV`: ``` > Sub_and_cond.COND_ELIM_CONV ``(\x. if b then f x else g...

Also, note that the changed `SUB_AND_COND_CONV` produces `x

Alternative to FORTRAN output (based on `unparse`): ``` Nasser wrote: > > newbie here. > I can't figure how to tell fricas to output result of command in 1D plain...

Updates: `)set message type off` can be used to disable the type printing of each output terms.

For the first time, `prove_real_assumsScript.sml` are fully commented and I'm glad to say that I finally understood every line in this file and the idea (of Ramana Kumar @xrchz) behind...

Now `realaxScript.sml` begins by calling `quotient.define_equivalence_type` to define the "real" type, and then the proof of a set of "primitive" real theorems just enough for `RealArith` package. All internal `TREAL`...

> Bravo. Thanks for doing all this and sorry my contributions weren't more easily decipherable. You're welcome (and thanks for your answers to all my related questions, mostly in private).

A new build of `hol4-large-numbers.art` (version 1.1) is available at https://www.dropbox.com/s/swgbu6bf1fehz7h/hol4-large-numbers-1.1.7z?dl=0 Some statistics: ``` Inference rules: eqMp ............... 6,103,723 subst .............. 5,161,610 deductAntisym ...... 4,954,952 appThm ............. 1,378,873 betaConv ................

> Sorry to have left this so long! It's OK (except that I was a little worry about your safety (and my future) ^_^)

I support the first idea. The "alternative" may cause ``(x ** 2) ** 3`` being printed as `“x²³”` which is even more confusing than `“R⁺ᵀ”`