On Tue, 30 Jul 2013, Josh Tilles wrote:
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?
It depends which part of the repository are affected. To get changes
accepted, someone who is an "expert" on that area of sources needs to
apply them. Finding out works by broadcasting here on this mailing list.
(Changes in main HOL are always critical, since almost everything else
depends on it, also performance-wise.)
EXPLANATION/DETAIL:
From what I've read in the documentation, structured Isar proofs are
preferred over apply-style proofs in every case except for
prototyping/experimentation.
Unstructured proof scripts (now called "apply style) and structured Isar
proofs are historically, technically, conceptually somehow related,
although in retrospect this is somehow accidental. The Isabelle/Isar
system was made in a way to include the old script style as "guest" to the
new approach. This worked so smoothly that people sometimes think that
Isar is still about "proof scripts", but it is actually about "proof
documents".
Moving back and forth between the two styles works for many Isabelle
experts after some practice, although my impression in recent years is
that it would be better to teach people just one style from the start, and
not pretend that one is a prerequisite to the other. (E.g. in
Isabelle2013 'by' no longer needs to be broken up into 1-2 'apply' to
diagnose its failure.)
There is a long story behind that, of how the system presents it by
default and how the manuals are written. And it is getting more and more
off-topic for isabelle-dev, which is about the development process, and
exploring / testing intermediate Isabelle snapshots between official
releases -- i.e. the everyday struggles with ongoing changes, not a
relaxed discussion about the big picture.
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
