src/HOL/ROOT
2015-12-05 nipkow 2015-12-05 added Brother12_Map
2015-12-04 nipkow 2015-12-04 added 1-2 brother trees
2015-11-24 traytel 2015-11-24 Ported old example to use (co)datatypes
2015-11-14 haftmann 2015-11-14 coalesce permanent_interpretation.ML with interpretation.ML
2015-11-02 wenzelm 2015-11-02 tuned document;
2015-10-30 nipkow 2015-10-30 added splay trees
2015-10-25 nipkow 2015-10-25 added 234-Trees (slow)
2015-10-18 nipkow 2015-10-18 added 2-3 trees (simpler and more complete than the version in ex/Tree23)
2015-10-09 kuncar 2015-10-09 add a file with examples of debugging transfer
2015-09-23 nipkow 2015-09-23 added AVL and lookup function
2015-09-22 nipkow 2015-09-22 added red black trees
2015-09-21 nipkow 2015-09-21 New subdirectory for functional data structures
2015-09-10 wenzelm 2015-09-10 HOL-Proofs is slow;
2015-09-09 Andreas Lochbihler 2015-09-09 reactivate examples with predicate compiler and quickcheck
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