Re: [Hol-info] library visibility

I recommend writing “uses” of modules/theories/libraries into your HOL script and copying those into your interactive HOL sessions with M-h M-r. A “use” is either an open declaration or the use of a qualified name. For example, writing fooTheory.bar_def and then using M-h M-r on that string wil

Re: [Hol-info] An infinite sum of 0 or 1 is finite, then ...

Thanks, my problem has been resolved using inductions. I'm actually using extrealTheory. All I have for the necessary and sufficient condition of a suminf being PosInf is the following: [ext_suminf_eq_infty] Theorem ⊢ ∀f. (∀n. 0 ≤ f n) ∧ (∀e. e < PosInf ⇒ ∃n. e ≤ ∑ f (count

[Hol-info] CICM 2019, July 8-12: Extended Deadline 8th March 2019 (abstracts), 15th March 2019 (full papers)

[Apologies for cross-postings] Call for Papers formal papers - informal papers - doctoral programme 12th Conference on Intelligent Computer Mathematics - CICM 2019 - July 8