2019-07-25 wenzelm more accurate proof definitions (PThm nodes);
2019-07-24 wenzelm avoid duplicate Thm.name_derivation on unnamed PThm nodes ("simps" vs. "case_eqns" and "recursor_eqns");
2019-07-24 wenzelm prefer local counter;
2019-07-24 wenzelm more accurate proof export;
2019-07-24 wenzelm clarified syntax;
2019-07-24 wenzelm tuned;
2019-07-24 wenzelm more thorough clean_proof;
2019-07-24 wenzelm clarified modules;
2019-07-24 wenzelm avoid global syntax for MinProof (amending e31271559de8);
2019-07-23 wenzelm treat MinProof like Promise before 725438ceae7c, e.g. relevant for performance of session Corec (due to Thm.derivation_closed/close_derivation);
2019-07-23 wenzelm discontinued Proofterm.Promise (cf. 725438ceae7c);
2019-07-23 wenzelm clarified treatment of unnamed PThm nodes (from close_derivation): retain full proof, publish when named;
2019-07-23 wenzelm tuned comments;
2019-07-23 wenzelm proof terms are always constructed sequentially;
2019-07-22 wenzelm tuned comments -- proper sections;
2019-07-22 wenzelm support export_proofs, prune_proofs;
2019-07-22 wenzelm clarified postproc: apply shrink_proof last, e.g. relevant for export of full proof term;
2019-07-22 wenzelm tuned;
2019-07-22 wenzelm clarified exception;
2019-07-22 wenzelm tuned;
2019-07-22 wenzelm more accurate type information;
2019-07-22 wenzelm unused (see also 42fbb6abed5a);
2019-07-21 wenzelm discontinued ASCII syntax;
2019-07-21 wenzelm global declaration of abstract syntax for proof terms, with qualified names;
2019-07-21 wenzelm tuned;
2019-07-21 wenzelm tuned;
2019-07-20 wenzelm more operations: support type classes within the logic;
2019-07-20 wenzelm clarified export of sort algebra: avoid logical operations in Isabelle/Scala;
2019-07-20 wenzelm more operations (avoid clones in Isabelle/MMT and Isabelle/Dedukti);
2019-07-20 wenzelm more robust: avoid folding of jEdit file-names wrt. JEDIT_SESSION_DIRS;
2019-07-19 paulson More results about measure and integration theory
2019-07-18 paulson More analysis / measure theory material
2019-07-18 paulson merged
2019-07-18 paulson more new material about analysis
2019-07-18 nipkow added forgotten declaration provided by Florian Haftmann
2019-07-17 wenzelm merged;
2019-07-17 wenzelm updated to jedit_build-20190717: support more brackets;
2019-07-17 wenzelm updated to isabelle_fonts-20190717;
2019-07-17 wenzelm redundant;
2019-07-17 wenzelm tuned;
2019-07-17 wenzelm added \<llangle>, \<rrangle>;
2019-07-17 wenzelm tuned doc isar-ref;
2019-07-17 wenzelm added \<bbar>;
2019-07-17 wenzelm added \<sqdot>;
2019-07-17 paulson fixed renaming issues
2019-07-17 paulson merged
2019-07-17 paulson a few new lemmas and a bit of tidying
2019-07-16 wenzelm support for a soft-type system within the Isabelle logical framework;
2019-07-11 nipkow tuned
2019-07-04 wenzelm proper theory naming after join (reset due to merge_data);
2019-07-04 wenzelm support join of anonymous theory nodes, e.g. relevant for parallel theory construction;
2019-07-04 wenzelm clarified history stage: allow independent updates that are merged later;
2019-06-24 wenzelm support abstract syntax for proof terms (see src/Pure/Proofs/proof_syntax.ML);
2019-06-23 haftmann proper quasi-total merge
2019-06-22 haftmann made LaTeX happy
2019-06-22 haftmann streamlined setup for linear algebra, particularly removed redundant rule declarations
2019-06-22 haftmann tuned
2019-06-21 haftmann tuned
2019-06-16 haftmann even more appropriate fact name
2019-06-16 haftmann more correct indicator
2019-06-14 haftmann make latex happy
2019-06-14 haftmann moved some theorems into HOL main corpus
2019-06-14 haftmann misc tuning and modernization
2019-06-14 haftmann more theorems for proof of concept for word type
(0) -30000 -10000 -3000 -1000 -300 -100 -64 +64 +100 +300 +1000 +3000 +10000 tip