2014-01-16 blanchet 2014-01-16 moved 'Zorn' into 'Main', since it's a BNF dependency
2014-01-10 traytel 2014-01-10 new codatatype example: stream processors
2013-11-18 blanchet 2013-11-18 compile
2013-11-18 blanchet 2013-11-18 split 'Cardinal_Arithmetic' 3-way
2013-11-18 blanchet 2013-11-18 started three-way split of 'HOL-Cardinals'
2013-11-16 wenzelm 2013-11-16 merged
2013-11-16 wenzelm 2013-11-16 proper thy_load command 'boogie_file' -- avoid direct access to file-system;
2013-11-14 haftmann 2013-11-14 explicit inclusion of data refinement theory into HOL-Library session
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);