Chun Tian
[Re Holinfo How to prove basic equivalency of rational.pdf](https://github.com/HOL-Theorem-Prover/HOL/files/7441360/Re.Holinfo.How.to.prove.basic.equivalency.of.rational.pdf) Here are some related email discussions in hol-info at the _beginning_ of 2019. I want to fix the entire `ratTheory` with...
> The existing code in `src/real` might be a guide to achieving this for the rationals. There are a surprisingly large number of rewrite theorems required to capture the various...
From the error messages it seems that OpenTheory's `fromNatural` should be the same thing as HOL4's `real_of_num`. Currently they are not mapped correctly.
There are also 2 irrelevant unsatisfied assumptions when installing `hol-ring`. Don't know which recent changes caused them but should be easy to fix: ``` opentheory install --reinstall hol4-ring.thy uninstalled package...
Q: What's the difference between "skipthm" and "delproof" in *.otd files? A (Ramana Kumar): They are orthogonal. looks like skipthm takes the theorem out of the exports, whereas delproof makes...
I'm glad to report that this issue has been fixed. Now I'm doing the whole build testing, will submit a PR soon.
4. `src/coalgebras/ltree.art` cannot be converted to `ltree.ot.art`. See https://github.com/HOL-Theorem-Prover/HOL/pull/958#issuecomment-950878372 for more details. NOTE: point 3 seems not true: HOL's OpenTheory reader can indeed _replay_ proofs stored in OpenTheory articles.
Copied from PR #1022: 5. `ordinalTheory` now contain workarounds for the definition of `ordDIV` and `ordMOD` as described already. If OpenTheory (or the exporting code in HOL) gets fixed in...
Hi, thanks for the additional information. I don't understand #642 but I tried the sample in #561: ``` ?!m. ((m = n) \/ m < n) /\ ((if m <...
Following the last piece of discussions in #1043. For the following example term in #6: ``` val tm = ``x - PRE i - SUC (PRE i - PRE i)...