Re: [Hol-info] build failed with latest HOL

Thanks..that solves the issue... On Mon, Oct 30, 2017 at 4:20 AM, wrote: > That’s a Poly/ML bug. Please use the 5.7 release available at > > > > https://github.com/polyml/polyml/archive/v5.7.tar.gz > > > > Michael > > > > *From: *Waqar Ahmad via hol-info

Re: [Hol-info] build failed with latest HOL

That’s a Poly/ML bug. Please use the 5.7 release available at https://github.com/polyml/polyml/archive/v5.7.tar.gz Michael From: Waqar Ahmad via hol-info Reply-To: Waqar Ahmad <12phdwah...@seecs.edu.pk> Date: Saturday, 28 October 2017 at 18:13 To: hol-info

Re: [Hol-info] How to define term-like multi-recursive structures?

You would have to define every function in terms of “fix” and then come up with a clause for the new constant using “Fix” as well (or prove a new “axiom” for the type). You would also need to prove new induction and cases theorems. But yes, this “cheap approach” might be doable. Michael On

Re: [Hol-info] Can the simplifier from simpLib normalize symmetric relations?

Passing the theorem EQ_SYM_EQ will normalise this sort of thing: > EQ_SYM_EQ; val it = |- ∀x y. x = y ⇔ y = x: thm > SIMP_CONV (srw_ss()) [EQ_SYM_EQ] “a = b ∧ x = z ⇔ b = a ∧ x = z”; <> val it = |- (a = b ∧ x = z ⇔ b = a ∧ x = z) ⇔ T: thm Michael On 29/10/17, 02:58, "Mario Castelán