On Wed, 24 Jun 2015, Makarius wrote:
After seeing too many "case 1", "case 2", "case 3" and corresponding
facts "1", "2", "3" I've now pushed this trivial change through, really
with rare incompatibilities.
Here is an example changeset that illustrates the reduction of odd digits
and redundancy in the source, for better proof mainainability:
http://isabelle.in.tum.de/repos/isabelle/rev/19c277ea65ae
I had already adapted these theories from HOL-Library and
HOL-Decision_Procs earlier, to make use of 'consider' and statements with
'if' / 'for'. Thus raw proof blocks with big-bang integration by blast
are mostly eliminated, and replaced by explicit proof structure.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
