On 03/12/16 14:57, Peter Lammich wrote: > > the attached theory is accepted by all Isabelle's from 2015 to the > latest 2016-1-RC4, without any complaints, even in batch mode > (isabelle build). > It just uses a prove_future, and proves the theorem with itself!
Here is the main result of investigating the sources and their entangled history: changeset: 64570:1134e4d5e5b7 user: wenzelm date: Fri Dec 16 19:07:16 2016 +0100 files: src/HOL/Library/Old_SMT/old_z3_proof_reconstruction.ML src/HOL/SPARK/Tools/spark_vcs.ML src/Pure/Thy/thy_info.ML src/Pure/more_thm.ML src/Pure/proofterm.ML src/Pure/thm.ML description: consolidate nested thms with persistent result, for improved performance; always consolidate parts of fulfill_norm_proof: important to exhibit cyclic thms (via non-termination as officially published), but this was lost in f33d5a00c25d; There was actually a second drop-out of formerly working behaviour (see a2e7862e7dd5), but the changeset 1134e4d5e5b7 subsumes both, because the consolidation of type thm/theory is now done a bit differently. General concepts behind all that are described in section 3.2 in my paper at ITP 2013, see especially the last two paragraphs. Dropouts of this category belong to the normal routine in Isabelle, according to its design principles in the last 10 years -- when we moved from a research experiment towards a serious system. System reliability has already reached a stage where most users never see it break down, so any sense of what can go wrong is lost. Hopefully this synthetic example helps to return to a better understanding of what Isabelle really is: an increasing approximation of ultimate perfection. Whenever we reach that, the system will be discarded :-) Makarius _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev