Re: [isabelle] "blast" eliminates unrelated flex-flex pairs in Isabelle2013-1 and Isabelle2013-2.



You shouldn’t have to redo the proofs. If you are lucky, doing the proof in Isabelle2013 may give you a clue as to how the variables are being instantiated, so that you can add a constraint somewhere. And flex-flex constraints are very rare.

Do you really have 400k lines of Isabelle proof scripts? All of the Isabelle/HOL theories (including examples and libraries) are barely more than that.

Larry Paulson


On 9 Dec 2013, at 21:47, David Greenaway <David.Greenaway at nicta.com.au> wrote:

> Alas, I am not the author of these thousands-of-line proofs, but merely
> the poor soul who is trying to get them working on Isabelle2013-2. The
> original authors have long since moved on to greener pastures.
> 
> While I agree it would be ideal to refactor the proof, one tends to take
> the path of least resistance when they have 400k lines of other proof
> script they also have to get working on the next Isabelle version...





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.