src/HOL/ROOT
2015-08-12 traytel 2015-08-12 actually process lift_bnf regression suite
2015-07-28 paulson 2015-07-28 the Cauchy integral theorem and related material
2015-07-27 haftmann 2015-07-27 formal class for factorial (semi)rings
2015-07-18 wenzelm 2015-07-18 reactivated dead code;
2015-06-12 bulwahn 2015-06-12 add examples from Freek's top 100 theorems (thms 30, 73, 77)
2015-06-14 wenzelm 2015-06-14 more examples;
2015-06-13 wenzelm 2015-06-13 more examples;
2015-06-01 wenzelm 2015-06-01 discontinued unused / unmaintained SVC oracle -- current Isabelle tools (e.g. arith, smt) can easily solve the given examples with full proof reconstruction;
2015-05-02 kuncar 2015-05-02 add testing file for code_dt extension of lifting
2015-04-17 wenzelm 2015-04-17 added Eisbach, using version 3752768caa17 of its Bitbucket repository;
2015-04-11 wenzelm 2015-04-11 make SML/NJ more happy;
2015-04-09 wenzelm 2015-04-09 make SML/NJ more happy;
2015-04-08 wenzelm 2015-04-08 proper test for session HOL-Library;
2015-04-03 wenzelm 2015-04-03 rearranged sessions to save approx. 1min elapsed time, 5min CPU time;
2015-04-01 wenzelm 2015-04-01 merged
2015-04-01 wenzelm 2015-04-01 clarified "main" group, e.g. relevant for Isabelle/jEdit menu;
2015-04-01 paulson 2015-04-01 John Harrison's example: a 32-bit approximation to pi. SLOW
2015-03-25 wenzelm 2015-03-25 HOL-SPARK .prv files are subject to system option spark_prv; tuned;
2015-03-23 nipkow 2015-03-23 BT subsumed by Library/Tree
2015-03-18 traytel 2015-03-18 bounded powerset
2015-03-18 paulson 2015-03-18 Merge
2015-03-18 paulson 2015-03-18 Lots of new material on complex-valued functions. Modified simplification of (x/n)^k
2015-03-18 noschinl 2015-03-18 added proof method rewrite
2015-03-10 paulson 2015-03-10 Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
2015-02-10 wenzelm 2015-02-10 check unused theory;
2015-01-25 wenzelm 2015-01-25 discontinued obsolete option "document_graph";
2014-12-28 kleing 2014-12-28 3 old example lemmas by Amine listed in the top 100 theorems
2014-12-20 wenzelm 2014-12-20 afford full test, with slightly improved scheduling order;
2014-12-17 hoelzl 2014-12-17 unfortunately, there is no general function space in the measurable spaces
2014-12-04 wenzelm 2014-12-04 more examples;
2014-11-14 wenzelm 2014-11-14 no quick_and_dirty for proof extraction, to avoid obscure errors like "corr: bad proof";
2014-10-31 wenzelm 2014-10-31 discontinued pointless option: timing is always on (overall theory only);
2014-10-31 wenzelm 2014-10-31 discontinued Proof General;
2014-10-10 nipkow 2014-10-10 New example Bubblesort
2014-10-08 wenzelm 2014-10-08 simplified "sos" method;
2014-10-08 Andreas Lochbihler 2014-10-08 move Code_Test to HOL/Library; add corresponding entries in NEWS and CONTRIBUTORS
2014-10-07 wenzelm 2014-10-07 more bibtex entries; more antiquotations;
2014-09-24 blanchet 2014-09-24 made N2M tests conditional, since they appear to cause Isatest timeouts and are kind of slow
2014-09-22 wenzelm 2014-09-22 clarified timeout for isatest;
2014-09-22 wenzelm 2014-09-22 examples for local CSDP executable;
2014-09-22 wenzelm 2014-09-22 clarified SOS tool setup vs. examples;
2014-09-22 wenzelm 2014-09-22 clarified ISABELLE_POLYML; added some isatests -- ISABELLE_SCALA still inactive due to problems with case-insensible file-system;
2014-09-21 wenzelm 2014-09-21 renamed ISABELLE_POLYML to ML_SYSTEM_POLYML, to avoid overlap with ISABELLE_POLYML_PATH;
2014-09-19 traytel 2014-09-19 regression tests for n2m
2014-09-18 blanchet 2014-09-18 moved 'old_datatype' out of 'Main' (but put it in 'HOL-Proofs' because of the inductive realizer) * * * made example compile again
2014-09-18 blanchet 2014-09-18 increased 'HOL-Proofs' timeout
2014-09-18 blanchet 2014-09-18 renamed SMT certificate files, following 'SMT2' -> 'SMT' renaming
2014-09-16 blanchet 2014-09-16 took out 'old_datatype' examples -- those just cause timeouts in Isatests
2014-09-12 blanchet 2014-09-12 enabled 'Sudoku' only with 'ISABELLE_FULL_TEST' -- Sudoku is fast enough on modern hardware (within seconds on my MacBook), but it seems to fail on older test machines
2014-09-12 blanchet 2014-09-12 run larger nominal examples only 'ISABELLE_FULL_TEST'
2014-09-11 blanchet 2014-09-11 renamed example theory for consistency
2014-09-11 blanchet 2014-09-11 updated ROOT
2014-09-11 blanchet 2014-09-11 renamed 'BNF_Examples' to 'Datatype_Examples' (cf. 'datatypes.pdf')
2014-09-11 blanchet 2014-09-11 move datatype benchmarks
2014-09-01 blanchet 2014-09-01 took out legacy material from 'HOL/Library/Library.thy'
2014-08-25 Andreas Lochbihler 2014-08-25 add testing framework for generated code
2014-08-22 haftmann 2014-08-22 generic euclidean algorithm (due to Manuel Eberl)
2014-08-19 Andreas Lochbihler 2014-08-19 rename Quickcheck_Types to Lattice_Constructions and remove quickcheck setup
2014-08-19 blanchet 2014-08-19 avoid old 'smt' method in examples
2014-07-24 wenzelm 2014-07-24 proper scope of comments;