src/HOL/ROOT
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);
2012-10-16 popescua 2012-10-16 update ROOT with teh directory change in BNF
2012-10-03 blanchet 2012-10-03 thread the right local theory through + reenable parallel proofs for previously problematic theories
2012-09-27 blanchet 2012-09-27 modernized examples; removed now trivial "HFset"
2012-09-26 blanchet 2012-09-26 disable parallel proofs for two big examples -- speeds up things and eliminates spurious Interrupt exceptions (to be investigated)
2012-09-21 blanchet 2012-09-21 changed base session for "HOL-BNF" for faster building in the typical case
2012-09-21 blanchet 2012-09-21 created separate session "HOL-BNF-LFP" as a step towards eventual integration in "HOL" in the middle term
2012-09-21 blanchet 2012-09-21 renamed "Codatatype" directory "BNF" (and corresponding session) -- this opens the door to no-nonsense session names like "HOL-BNF-LFP"
2012-09-20 blanchet 2012-09-20 the Codatatype package currently needs all of Cardinals (temporary -- because of countable sets)
2012-09-19 wenzelm 2012-09-19 reactivate HOL-Mirabelle-ex with increased chances that it works most of the time (cf. bec1add86e79, a93d920707bb, be27a453aacc);
2012-09-18 popescua 2012-09-18 added top-level theory for Cardinals
2012-09-17 wenzelm 2012-09-17 bypass HOL-Mirabelle-ex in regular test, until its tendency to "hang" has been resolved;
2012-09-13 wenzelm 2012-09-13 workaround for HOL-Mirabelle-ex oddities;