src/HOL/ROOT
2017-04-24 wenzelm 2017-04-24 recovered document from 0f3fdf689bf9;
2017-04-24 wenzelm 2017-04-24 clarified parent session images, to avoid duplicate loading of theories; avoid name conflict with loaded theory src/HOL/Library/Parallel.thy;
2017-04-24 wenzelm 2017-04-24 clarified parent session images, to avoid duplicate loading of theories;
2017-04-23 wenzelm 2017-04-23 actually use theory;
2017-04-23 wenzelm 2017-04-23 clarified parent session images, to avoid duplicate loading of theories;
2017-04-23 wenzelm 2017-04-23 actually use theory; tuned;
2017-04-23 wenzelm 2017-04-23 renamed theory to avoid conflict with loaded theory "Tree" from HOL-Library;
2017-04-22 wenzelm 2017-04-22 theories "GCD" and "Binomial" are already included in "Main": this avoids improper imports in applications;
2017-04-22 wenzelm 2017-04-22 clarified parent session images, to avoid duplicate loading of theories;
2017-04-21 wenzelm 2017-04-21 tuned;
2017-04-21 wenzelm 2017-04-21 removed pointless document;
2017-04-21 wenzelm 2017-04-21 merged
2017-04-21 wenzelm 2017-04-21 clarified session imports;
2017-04-21 wenzelm 2017-04-21 tuned imports;
2017-04-21 wenzelm 2017-04-21 clarified imports;
2017-04-21 wenzelm 2017-04-21 include imports that morally belong to Main and are used in HOL-Proofs applications;
2017-04-20 blanchet 2017-04-20 removed Old_SMT legacy module
2017-04-19 wenzelm 2017-04-19 clarified session structure: avoid ambiguity of file ~~/src/HOL/Library/Old_Datatype.thy;
2017-04-17 haftmann 2017-04-17 consistent session name
2017-04-11 wenzelm 2017-04-11 less global theories -- conflict with AFP entries;
2017-04-10 wenzelm 2017-04-10 explicit theory qualifier for session "HOL-Proofs": its theory name space overlaps with session "HOL", even for further imports;
2017-04-09 wenzelm 2017-04-09 added system option record_proofs, which allows to build HOL-Proofs without special Proofs.thy;
2017-04-06 haftmann 2017-04-06 session containing computational algebra
2017-04-06 haftmann 2017-04-06 more approproiate placement of theories MiscAlgebra and Multiplicate_Group
2017-04-04 wenzelm 2017-04-04 more main sessions and global theories;
2017-04-04 wenzelm 2017-04-04 eliminated redundant imports;
2017-04-04 wenzelm 2017-04-04 eliminated Plain_HOLCF.thy (see also 8e92772bc0e8): it was modeled after HOL/Plain.thy which was discontinued later;
2017-04-04 wenzelm 2017-04-04 tuned;
2017-04-04 wenzelm 2017-04-04 tuned syntax; some official documentation;
2017-03-02 ballarin 2017-03-02 Knaster-Tarski fixed point theorem and Galois Connections.
2017-02-26 haftmann 2017-02-26 re-established AFP entry for FinFuns as library
2017-02-02 blanchet 2017-02-02 added veriT preprocessing proof reconstruction example
2017-01-27 haftmann 2017-01-27 ML antiquotation for generated computations
2017-01-18 wenzelm 2017-01-18 clarified theory name; tuned;
2017-01-13 eberlm 2017-01-13 Added Circle_Area to HOL-Analysis examples
2016-12-18 wenzelm 2016-12-18 test parallel proof terms in this small session (somewhat slow for bigger applications);
2016-12-17 haftmann 2016-12-17 restructured matter on polynomials and normalized fractions
2016-12-17 haftmann 2016-12-17 clarified library contents
2016-12-17 wenzelm 2016-12-17 unconditional Code_Test_PolyML and Code_Test_Scala: compiler is always present;
2016-12-14 wenzelm 2016-12-14 simplified options;
2016-12-12 wenzelm 2016-12-12 merged
2016-12-12 wenzelm 2016-12-12 proper session HOL-Types_To_Sets; NEWS; CONTRIBUTORS; tuned whitespace;
2016-11-23 nipkow 2016-11-23 moved IMP/Abs_Int_ITP to AFP/Abs_Int_ITP2012
2016-10-30 kuncar 2016-10-30 types to sets: initial commit
2016-10-24 blanchet 2016-10-24 added Nunchaku integration
2016-10-24 traytel 2016-10-24 additional user-specified simp (naturality) rules used in friend_of_corec
2016-10-20 nipkow 2016-10-20 tuned
2016-10-17 eberlm 2016-10-17 Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
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.