Changes

Changes from Mercurial (hg http://isabelle.in.tum.de/repos/isabelle/ default)

Summary

merged
proper build_selection for clean_build (amending 961285f581e6): e.g. relevant for "isabelle build_doc";
clarified signature (again);
clarified exclusion: operate on completed selection, as last step;
tuned;
tuned signature;
clarifified selection: always wrt. build_graph structure; tuned signature;
tuned;
tuned signature;
more robust parsing for THF proofs (esp. polymorphic Leo-III proofs)
integrated Leo-III in Sledgehammer (thanks to Alexander Steen for the patch)
added FIXMEs
Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
backed out odd "bug fix" 671decd2e627;
more recent polyml-test version; afford more heap by default: all platforms are now 64bit and presumably have sufficient memory;
minimal document model for theory files;
tuned signature;

Changeset 67031:22a47374a205 by wenzelm: merged
Changeset 67030:a9859e879f38 by wenzelm: proper build_selection for clean_build (amending 961285f581e6): e.g. relevant for "isabelle build_doc";
The file was modified	`src/Pure/Tools/build.scala`
Changeset 67029:d6d9fd2559ce by wenzelm: clarified signature (again);
The file was modified	`src/Pure/Thy/sessions.scala`
Changeset 67028:c4e678c2df3c by wenzelm: clarified exclusion: operate on completed selection, as last step;
The file was modified	`src/Pure/Thy/sessions.scala`
Changeset 67027:d4f245bea081 by wenzelm: tuned;
The file was modified	`src/Pure/Thy/sessions.scala`
Changeset 67026:687c822ee5e3 by wenzelm: tuned signature;
The file was modified	`src/Pure/Admin/afp.scala`
The file was modified	`src/Pure/Admin/build_doc.scala`
The file was modified	`src/Pure/ML/ml_process.scala`
The file was modified	`src/Pure/Thy/sessions.scala`
The file was modified	`src/Pure/Tools/build.scala`
The file was modified	`src/Pure/Tools/imports.scala`
The file was modified	`src/Tools/jEdit/src/jedit_sessions.scala`
Changeset 67025:961285f581e6 by wenzelm: clarifified selection: always wrt. build_graph structure;<br>tuned signature;
The file was modified	`src/Pure/Admin/afp.scala`
The file was modified	`src/Pure/ML/ml_process.scala`
The file was modified	`src/Pure/Thy/sessions.scala`
The file was modified	`src/Pure/Tools/build.scala`
The file was modified	`src/Pure/Tools/imports.scala`
Changeset 67024:72d37a2e9cca by wenzelm: tuned;
The file was modified	`src/Pure/Thy/sessions.scala`
The file was modified	`src/Tools/jEdit/src/jedit_sessions.scala`
Changeset 67023:e27e05d6f2a7 by wenzelm: tuned signature;
The file was modified	`src/Pure/Admin/build_doc.scala`
The file was modified	`src/Pure/Thy/sessions.scala`
The file was modified	`src/Pure/Tools/imports.scala`
The file was modified	`src/Tools/jEdit/src/jedit_sessions.scala`
Changeset 67022:49309fe530fd by blanchet: more robust parsing for THF proofs (esp. polymorphic Leo-III proofs)
The file was modified	`src/HOL/Tools/ATP/atp_proof.ML`
The file was modified	`src/HOL/Tools/ATP/atp_satallax.ML`
Changeset 67021:41f1f8c4259b by blanchet: integrated Leo-III in Sledgehammer (thanks to Alexander Steen for the patch)
The file was modified	`src/Doc/Sledgehammer/document/root.tex`
The file was modified	`src/Doc/manual.bib`
The file was modified	`src/HOL/Tools/ATP/atp_proof.ML`
The file was modified	`src/HOL/Tools/ATP/atp_systems.ML`
Changeset 67020:c32254ab1901 by blanchet: added FIXMEs
The file was modified	`src/HOL/Library/Multiset_Order.thy`
Changeset 67019:7a3724078363 by nipkow: Replaced { } proofs by local lemmas; added Hoare logic with logical variables.
The file was added	`src/HOL/IMP/Hoare_Total_EX2.thy`
The file was added	`src/HOL/IMP/VCG_Total_EX2.thy`
The file was modified	`src/HOL/IMP/Abs_Int3.thy`
The file was modified	`src/HOL/IMP/Big_Step.thy`
The file was modified	`src/HOL/IMP/Compiler2.thy`
The file was modified	`src/HOL/IMP/Denotational.thy`
The file was modified	`src/HOL/IMP/Hoare_Sound_Complete.thy`
The file was modified	`src/HOL/IMP/Hoare_Total.thy`
The file was modified	`src/HOL/IMP/Hoare_Total_EX.thy`
The file was modified	`src/HOL/IMP/Live_True.thy`
The file was modified	`src/HOL/IMP/VCG_Total_EX.thy`
The file was modified	`src/HOL/ROOT`
Changeset 67018:f6aa133f9b16 by wenzelm: backed out odd "bug fix" 671decd2e627;
The file was modified	`src/Pure/General/graph.scala`
The file was modified	`src/Pure/Thy/sessions.scala`
Changeset 67017:ce6454669360 by wenzelm: more recent polyml-test version;<br>afford more heap by default: all platforms are now 64bit and presumably have sufficient memory;
The file was modified	`Admin/components/components.sha1`
The file was modified	`Admin/components/main`
The file was modified	`Admin/polyml/settings`
Changeset 67016:57d58c3cf16b by wenzelm: minimal document model for theory files;
The file was added	`src/Pure/Thy/thy_document_model.scala`
The file was modified	`src/Pure/build-jars`
Changeset 67015:1a9e2a2bf251 by wenzelm: tuned signature;
The file was modified	`src/Pure/PIDE/resources.scala`
The file was modified	`src/Tools/VSCode/src/vscode_resources.scala`