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



On 10/12/13 00:57, Lawrence Paulson wrote:
> If you get these constraints in a proof, even if it currently works,
> it might be a good idea to look for a different proof (by explicitly
> instantiating a variable that is currently left uninstantiated) to get
> rid of them yourself.

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...

Cheers,
David


________________________________

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.




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