src/HOL/ROOT
2014-03-07 wenzelm 2014-03-07 tuned whitespace;
2014-02-24 paulson 2014-02-24 Gauss.thy ported from Old_Number_Theory (unfinished)
2014-02-21 wenzelm 2014-02-21 more standard theory name;
2014-02-19 haftmann 2014-02-19 offical tool
2014-02-19 sultana 2014-02-19 reconstruction framework for LEO-II's TPTP proofs;
2014-02-13 wenzelm 2014-02-13 reactivate some examples that still appear to work;
2014-02-13 wenzelm 2014-02-13 do not redefine outer syntax commands;
2014-02-12 blanchet 2014-02-12 adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems * * * more transition of 'xxx_rec' to 'rec_xxx' and same for case * * * compile * * * 'rename_tac's to avoid referring to generated names * * * more robust scripts with 'rename_tac' * * * 'where' -> 'of' * * * 'where' -> 'of' * * * renamed 'xxx_rec' to 'rec_xxx'
2014-02-09 wenzelm 2014-02-09 minimal document;
2014-02-04 paulson 2014-02-04 Restoration of Pocklington.thy. Tidying.
2014-02-01 wenzelm 2014-02-01 proper config options; proper context for printing;
2014-01-29 paulson 2014-01-29 Replacing the theory Library/Binomial by Number_Theory/Binomial
2014-01-23 wenzelm 2014-01-23 no document for Cartouche_Examples: avoid problems typesetting "\001";
2014-01-20 blanchet 2014-01-20 dissolved BNF session
2014-01-20 blanchet 2014-01-20 minimized Nitpick's dependencies
2014-01-20 blanchet 2014-01-20 moved BNF examples
2014-01-20 blanchet 2014-01-20 killed obsolete session
2014-01-20 blanchet 2014-01-20 moved subset of 'HOL-Cardinals' needed for BNF into 'HOL'
2014-01-18 wenzelm 2014-01-18 support for nested text cartouches; clarified Symbol.is_symbolic: exclude \<open> and \<close>;
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