src/HOL/ROOT
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;
2012-09-12 blanchet 2012-09-12 renamed "Ordinals_and_Cardinals" to "Cardinals"
2012-09-04 traytel 2012-09-04 eliminated obsolete "parallel_proofs = 0" restriction (cf. 0e5b859e1c91)
2012-08-29 Christian Sternagel 2012-08-29 renamed theory List_Prefix into Sublist (since it is not only about prefixes)
2012-08-28 wenzelm 2012-08-28 do not hardwire document output options -- to be provided by the user;
2012-08-28 blanchet 2012-08-28 tuning
2012-08-28 blanchet 2012-08-28 documentation cleanup
2012-08-28 blanchet 2012-08-28 added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
2012-08-19 wenzelm 2012-08-19 actual use of (sos remote_csdp) via ISABELLE_FULL_TEST;
2012-08-23 wenzelm 2012-08-23 more basic file dependencies -- no load command here;
2012-08-11 nipkow 2012-08-11 special code with lists no longer necessary, use sets
2012-08-08 wenzelm 2012-08-08 simplified session specifications: names are taken verbatim and current directory is default;
2012-08-07 wenzelm 2012-08-07 tuned;
2012-08-06 wenzelm 2012-08-06 more precise imitation of old ROOT.ML files;
2012-08-04 wenzelm 2012-08-04 some timeouts, which modify the build order;
2012-08-01 wenzelm 2012-08-01 added offline test for skip_proofs;