src/HOL/ROOT
2013-10-23 blanchet 2013-10-23 added 'primcorec' examples
2013-09-26 wenzelm 2013-09-26 added Isabelle/ML example;
2013-09-24 blanchet 2013-09-24 register codatatypes with Nitpick
2013-09-17 kuncar 2013-09-17 include Int_Pow into Quotient_Examples; add end of the theory
2013-09-06 noschinl 2013-09-06 added examples for Simps_Case_Conv
2013-08-30 blanchet 2013-08-30 added example
2013-08-23 wenzelm 2013-08-23 clarified position of Spec_Check for Isabelle/ML -- it is unrelated to Isabelle/HOL; just one src/Tools/ROOT;
2013-08-21 blanchet 2013-08-21 renamed theory files to be closer to (new) command names
2013-07-24 nipkow 2013-07-24 merged Def_Init_Sound_X into Def_Init_X
2013-07-23 boehmes 2013-07-23 removed obsolete HOL-Boogie session; keep examples that also test SMT solvers, using a minimal version of the old Boogie loader
2013-07-02 wenzelm 2013-07-02 clarified Proofterm.proofs vs. Goal.skip_proofs;
2013-06-30 wenzelm 2013-06-30 discontinued system option "proofs" -- global state of Proofterm.proofs is persistently compiled into HOL-Proofs image; discontinued unused proofterms for FOL;
2013-06-23 wenzelm 2013-06-23 support for XML data representation of proof terms;
2013-06-20 nipkow 2013-06-20 tuned theory name
2013-06-19 nipkow 2013-06-19 more canonical name (2)
2013-06-10 haftmann 2013-06-10 dropped relics of ancient binary numeral case study
2013-06-01 nipkow 2013-06-01 tuned theory name
2013-05-31 wenzelm 2013-05-31 make SML/NJ partially happy;
2013-05-31 nipkow 2013-05-31 more VC -> VCG
2013-05-30 bulwahn 2013-05-30 added Spec_Check -- a Quickcheck tool for Isabelle's ML environment;
2013-05-29 wenzelm 2013-05-29 obsolete;
2013-04-05 nipkow 2013-04-05 tuned document
2013-03-27 wenzelm 2013-03-27 separate isatest with skip_proofs, to give some impression of performance without most of the proofs;
2013-03-27 wenzelm 2013-03-27 tuned;
2013-03-27 wenzelm 2013-03-27 allow build with skip_proofs enabled -- disable it for sessions that would fail due to embedded diagnostic commands, for example;
2013-03-27 wenzelm 2013-03-27 more ambitious Goal.skip_proofs: covers Goal.prove forms as well, and do not insist in quick_and_dirty (for the sake of Isabelle/jEdit);
2013-03-26 wenzelm 2013-03-26 tuned session specification;
2013-03-25 ballarin 2013-03-25 Discontinued theories src/HOL/Algebra/abstract and .../poly.
2013-03-13 wenzelm 2013-03-13 proper formatting, to facilitate line-based diff;
2013-03-13 wenzelm 2013-03-13 more uniform session descriptions, which show up in chapter index;
2013-03-12 wenzelm 2013-03-12 refurbished some old README.html files as session descriptions, which show up in chapter index;
2013-03-11 wenzelm 2013-03-11 support for 'chapter' specifications within session ROOT;
2013-02-24 haftmann 2013-02-24 turned example into library for comparing growth of functions
2013-02-21 wenzelm 2013-02-21 more explicit session dependency, for improved parallel performance of HOL-UNITY test session -- NB: separate 'theories' sections are sequential;
2013-02-15 haftmann 2013-02-15 attempt to re-establish conventions which theories are loaded into the grand unified library theory; four different code generation tests for different code setup constellations; augment code generation setup where necessary
2013-02-15 haftmann 2013-02-15 systematic conversions between nat and nibble/char; more uniform approaches to execute operations on nibble/char
2013-02-15 haftmann 2013-02-15 two target language numeral types: integer and natural, as replacement for code_numeral; former theory HOL/Library/Code_Numeral_Types replaces HOL/Code_Numeral; refined stack of theories implementing int and/or nat by target language numerals; reduced number of target language numeral types to exactly one
2013-02-14 haftmann 2013-02-14 consolidation of library theories on product orders
2013-02-13 haftmann 2013-02-13 tuned, particulary name
2013-01-19 wenzelm 2013-01-19 afford parallel proof terms;
2013-01-13 wenzelm 2013-01-13 hardwired document_variants, to prevent HOL-IMP's \snip choking on macros from isabellestags.sty;
2013-01-12 wenzelm 2013-01-12 populate "main" session group, e.g. relevant for Isabelle/jEdit logic selection;
2013-01-11 wenzelm 2013-01-11 discontinued HOL side-entry sessions -- may be configured in $ISABELLE_HOME_USER/ROOT instead;
2013-01-02 blanchet 2013-01-02 actually run Z3 for "SMT_Tests" when "ISABELLE_FULL_TEST" is enabled
2013-01-02 blanchet 2013-01-02 added missing certificate file to "ROOT"
2012-12-29 nipkow 2012-12-29 new theory Library/Finite_Lattice
2012-12-16 wenzelm 2012-12-16 HOL-Quickcheck_Benchmark works without timeout (NB: isatest imposes global timeout already);
2012-12-16 bulwahn 2012-12-16 reverting d466ebc27810 as the previous changeset should allow to run Find_Unused_Assms_Examples again
2012-12-13 traytel 2012-12-13 renamed theory
2012-12-11 wenzelm 2012-12-11 disable Find_Unused_Assms_Examples for now, to recover isatest sanity;
2012-12-04 hoelzl 2012-12-04 remove SMT proofs in Multivariate_Analysis
2012-11-23 wenzelm 2012-11-23 timeout in proper place (HOL-Quickcheck_Examples approx. 1min, HOL-Quickcheck_Benchmark approx. 1h);
2012-11-22 nipkow 2012-11-22 tuned names
2012-11-21 wenzelm 2012-11-21 more generous timeout for SML/NJ, which is approx. 40-80 times slower than Poly/ML; more generous timeout for HOL-Quickcheck_Examples, which is rather slow in checking its examples (and mostly sequential);
2012-11-21 nipkow 2012-11-21 new theory of immutable arrays
2012-11-12 nipkow 2012-11-12 new theory IMP/Finite_Reachable
2012-11-08 haftmann 2012-11-08 refined stack of library theories implementing int and/or nat by target language numerals
2012-10-31 blanchet 2012-10-31 moved Refute to "HOL/Library" to speed up building "Main" even more
2012-10-18 wenzelm 2012-10-18 back to parallel HOL-BNF-Examples, which seems to have suffered from Future.map on canceled persistent futures;
2012-10-17 wenzelm 2012-10-17 HOL-BNF-Examples is sequential for now, due to spurious interrupts (again);