src/HOL/ROOT
2016-03-24 nipkow 2016-03-24 added Leftist_Heap
2016-03-22 blanchet 2016-03-22 added 'corec' examples and tests
2016-03-22 blanchet 2016-03-22 added two 'corec' examples
2016-02-29 wenzelm 2016-02-29 clarified session; tuned headers;
2016-02-23 nipkow 2016-02-23 was only of historical interest anymore
2016-02-19 wenzelm 2016-02-19 moved examples to avoid dependency on bulky HOL-Proofs session, e.g. relevant for "isabelle makedist";
2016-02-17 wenzelm 2016-02-17 merged
2016-02-17 wenzelm 2016-02-17 SML/NJ is no longer supported;
2016-02-17 haftmann 2016-02-17 separated potentially conflicting type class instance into separate theory
2016-02-13 wenzelm 2016-02-13 clarified ISABELLE_FULL_TEST vs. benchmarks: src/Benchmarks is not in ROOTS and thus not covered by "isabelle build -a" by default;
2016-02-13 wenzelm 2016-02-13 unconditional test -- nothing special here;
2016-01-24 wenzelm 2016-01-24 guard sessions that no longer work with SML/NJ -- memory problems;
2016-01-13 wenzelm 2016-01-13 Eisbach works for other object-logics, e.g. Eisbach_FOL.thy;
2016-01-12 wenzelm 2016-01-12 merged
2016-01-12 wenzelm 2016-01-12 removed in anticipation of c92d82c3f41b -- demolition after renovation;
2016-01-12 traytel 2016-01-12 removed outdated example
2016-01-11 nipkow 2016-01-11 added AA_Map; tuned titles
2015-12-31 wenzelm 2015-12-31 clarified directory structure;
2015-12-27 haftmann 2015-12-27 put example into separate session, to restrict precious session image to library theories
2015-12-27 wenzelm 2015-12-27 tuned document;
2015-12-27 wenzelm 2015-12-27 more proofs;
2015-12-26 wenzelm 2015-12-26 clarified sessions;
2015-12-06 nipkow 2015-12-06 added AA trees
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