Dear all,
As you might know, Andrei Popescu, Dmitriy Traytel, and I have been working on a
new (co)datatype package. It is part of Isabelle2013 in the directory
src/HOL/Tools/BNF (BNF = bounded natural functors) [1]. The package is
described in some detail in our LICS 2012 paper [2].
The package
QUESTION STATED BRIEFLY:
If I convert existing proofs in src/HOL/**.thy from apply-style to
Isar-style, would those changes be welcome in the main repository?
EXPLANATION/DETAIL:
From what I've read in the documentation, structured Isar proofs are
preferred over apply-style proofs in every case
The Isabelle checkpoints are gone:
http://isabelle.in.tum.de/reports/Isabelle/rev/da1fdbfebd39
This is reminiscent of how the West Goths resolved their problems at the
Eastern Goths' customer clearance checkpoint:
http://isabelle.in.tum.de/~haftmann/img/sledgehammer.gif
Florian
--
This could be a valuable service, especially for long lists of applys. (A proof
like by (induct n) auto should be left alone.)
Do ask an experienced user to examine your early attempts for beginner's
mistakes, like labelling all intermediate results.
Larry
On 30 Jul 2013, at 18:40, Josh
