Re: [isabelle] "blast" eliminates unrelated flex-flex pairs in Isabelle2013-1 and Isabelle2013-2.
On 11/12/13 08:42, Lawrence Paulson wrote:
> 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.
Again, these tend to pop up in very large proofs which I have very
little understanding or context of. Add in a few moving parts, such as
Schirmer's SIMPL VCG , our own tactics (for example, bundled with
), and ugly proofs done on a deadline, it all becomes a bit much.
Tracking down the original problem involved carefully comparing
line-by-line the proof output between Isabelle2013 and Isabelle2013-1
and seeing where they diverged.
I am certainly not advocating this proof style, merely trying to cope
> 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.
~/l4.verified # rm -rf isabelle
~/l4.verified # wc -l **/*.thy | tail -1
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