src/HOL/ROOT
2016-10-03 haftmann 2016-10-03 proof of concept for algebraically founded word types
2016-10-01 wenzelm 2016-10-01 Isar proof of Schroeder_Bernstein without using Hilbert_Choice (and metis);
2016-09-29 boehmes 2016-09-29 new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
2016-09-19 kuncar 2016-09-19 resolve the name clash of HOL/Library/FSet and HOL/Quotient_Examples/FSet
2016-09-16 wenzelm 2016-09-16 sessions that are relevant for routine timing measurements;
2016-09-15 Lars Hupel 2016-09-15 new type for finite maps; use it in HOL-Probability
2016-09-09 nipkow 2016-09-09 More on balancing; renamed theory to Balance
2016-09-08 wenzelm 2016-09-08 option "checkpoint" helps to fine-tune global heap space management;
2016-09-01 wenzelm 2016-09-01 clarified session: use all theories in directory HOL/Library;
2016-09-01 blanchet 2016-09-01 added theory to provide workaround to support nested datatypes in quickcheck (until quickcheck is generalized to support it with new datatypes)
2016-08-09 nipkow 2016-08-09 New theory Balance_List
2016-08-08 hoelzl 2016-08-08 rename HOL-Multivariate_Analysis to HOL-Analysis.
2016-08-04 hoelzl 2016-08-04 HOL-Multivariate_Analysis: rename theories for more descriptive names
2016-07-23 nipkow 2016-07-23 added new vcg based on existentially quantified while-rule
2016-07-22 eberlm 2016-07-22 Removed redundant material related to primes
2016-07-13 eberlm 2016-07-13 Reformed factorial rings
2016-07-04 haftmann 2016-07-04 basic facts about almost everywhere fix bijections
2016-06-10 wenzelm 2016-06-10 bundles "finfun_syntax" and "no_finfun_syntax" for optional syntax;
2016-05-31 blanchet 2016-05-31 added test
2016-05-26 haftmann 2016-05-26 examples and documentation for code generator time measurements
2016-05-13 wenzelm 2016-05-13 more complete theories;
2016-05-10 paulson 2016-05-10 Theory of polyhedra: faces, extreme points, polytopes, and the Krein–Milman Minkowski theorem
2016-05-01 nipkow 2016-05-01 the standard While-rule
2016-04-17 Lars Hupel 2016-04-17 remove "slow" session tags
2016-04-17 wenzelm 2016-04-17 misc tuning and modernization;
2016-04-15 Lars Hupel 2016-04-15 add "slow" group to descendants of HOL-Proofs
2016-03-28 blanchet 2016-03-28 another 'corec' example
2016-03-28 blanchet 2016-03-28 new 'corec' example
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