src/HOL/ROOT
Sun, 23 Apr 2017 23:54:06 +0200 wenzelm actually use theory;
Sun, 23 Apr 2017 23:49:14 +0200 wenzelm clarified parent session images, to avoid duplicate loading of theories;
Sun, 23 Apr 2017 19:06:53 +0200 wenzelm actually use theory;
Sun, 23 Apr 2017 18:54:18 +0200 wenzelm renamed theory to avoid conflict with loaded theory "Tree" from HOL-Library;
Sat, 22 Apr 2017 22:01:35 +0200 wenzelm theories "GCD" and "Binomial" are already included in "Main": this avoids improper imports in applications;
Sat, 22 Apr 2017 12:52:16 +0200 wenzelm clarified parent session images, to avoid duplicate loading of theories;
Fri, 21 Apr 2017 21:41:32 +0200 wenzelm tuned;
Fri, 21 Apr 2017 21:36:49 +0200 wenzelm removed pointless document;
Fri, 21 Apr 2017 20:36:20 +0200 wenzelm merged
Fri, 21 Apr 2017 20:07:51 +0200 wenzelm clarified session imports;
Fri, 21 Apr 2017 16:48:58 +0200 wenzelm tuned imports;
Fri, 21 Apr 2017 16:12:11 +0200 wenzelm clarified imports;
Fri, 21 Apr 2017 11:38:45 +0200 wenzelm include imports that morally belong to Main and are used in HOL-Proofs applications;
Thu, 20 Apr 2017 16:21:28 +0200 blanchet removed Old_SMT legacy module
Wed, 19 Apr 2017 15:53:58 +0200 wenzelm clarified session structure: avoid ambiguity of file ~~/src/HOL/Library/Old_Datatype.thy;
Mon, 17 Apr 2017 07:44:21 +0200 haftmann consistent session name
Tue, 11 Apr 2017 16:18:01 +0200 wenzelm less global theories -- conflict with AFP entries;
Mon, 10 Apr 2017 13:30:55 +0200 wenzelm explicit theory qualifier for session "HOL-Proofs": its theory name space overlaps with session "HOL", even for further imports;
Sun, 09 Apr 2017 20:17:00 +0200 wenzelm added system option record_proofs, which allows to build HOL-Proofs without special Proofs.thy;
Thu, 06 Apr 2017 21:37:13 +0200 haftmann session containing computational algebra
Thu, 06 Apr 2017 08:33:37 +0200 haftmann more approproiate placement of theories MiscAlgebra and Multiplicate_Group
Tue, 04 Apr 2017 22:16:42 +0200 wenzelm more main sessions and global theories;
Tue, 04 Apr 2017 22:07:34 +0200 wenzelm eliminated redundant imports;
Tue, 04 Apr 2017 21:57:43 +0200 wenzelm eliminated Plain_HOLCF.thy (see also 8e92772bc0e8): it was modeled after HOL/Plain.thy which was discontinued later;
Tue, 04 Apr 2017 21:11:40 +0200 wenzelm tuned;
Tue, 04 Apr 2017 21:05:07 +0200 wenzelm tuned syntax;
Thu, 02 Mar 2017 21:16:02 +0100 ballarin Knaster-Tarski fixed point theorem and Galois Connections.
Sun, 26 Feb 2017 13:22:14 +0100 haftmann re-established AFP entry for FinFuns as library
Thu, 02 Feb 2017 14:42:06 +0100 blanchet added veriT preprocessing proof reconstruction example
Fri, 27 Jan 2017 22:27:03 +0100 haftmann ML antiquotation for generated computations
Wed, 18 Jan 2017 17:56:52 +0100 wenzelm clarified theory name;
Fri, 13 Jan 2017 17:45:51 +0100 eberlm Added Circle_Area to HOL-Analysis examples
Sun, 18 Dec 2016 13:46:57 +0100 wenzelm test parallel proof terms in this small session (somewhat slow for bigger applications);
Sat, 17 Dec 2016 15:22:13 +0100 haftmann restructured matter on polynomials and normalized fractions
Sat, 17 Dec 2016 15:22:13 +0100 haftmann clarified library contents
Sat, 17 Dec 2016 14:47:41 +0100 wenzelm unconditional Code_Test_PolyML and Code_Test_Scala: compiler is always present;
Wed, 14 Dec 2016 18:37:54 +0100 wenzelm simplified options;
Mon, 12 Dec 2016 17:40:06 +0100 wenzelm merged
Mon, 12 Dec 2016 11:33:14 +0100 wenzelm proper session HOL-Types_To_Sets;
Wed, 23 Nov 2016 16:28:42 +0100 nipkow moved IMP/Abs_Int_ITP to AFP/Abs_Int_ITP2012
Sun, 30 Oct 2016 13:15:14 +0100 kuncar types to sets: initial commit
Mon, 24 Oct 2016 22:42:07 +0200 blanchet added Nunchaku integration
Mon, 24 Oct 2016 16:53:32 +0200 traytel additional user-specified simp (naturality) rules used in friend_of_corec
Thu, 20 Oct 2016 19:39:27 +0200 nipkow tuned
Mon, 17 Oct 2016 15:20:06 +0200 eberlm Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
Mon, 03 Oct 2016 14:37:06 +0200 haftmann proof of concept for algebraically founded word types
Sat, 01 Oct 2016 17:38:14 +0200 wenzelm Isar proof of Schroeder_Bernstein without using Hilbert_Choice (and metis);
Thu, 29 Sep 2016 20:54:44 +0200 boehmes new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
Mon, 19 Sep 2016 23:14:34 +0200 kuncar resolve the name clash of HOL/Library/FSet and HOL/Quotient_Examples/FSet
Fri, 16 Sep 2016 15:54:50 +0200 wenzelm sessions that are relevant for routine timing measurements;
Thu, 15 Sep 2016 22:41:05 +0200 Lars Hupel new type for finite maps; use it in HOL-Probability
Fri, 09 Sep 2016 14:15:16 +0200 nipkow More on balancing; renamed theory to Balance
Thu, 08 Sep 2016 18:18:57 +0200 wenzelm option "checkpoint" helps to fine-tune global heap space management;
Thu, 01 Sep 2016 21:28:46 +0200 wenzelm clarified session: use all theories in directory HOL/Library;
Thu, 01 Sep 2016 12:10:52 +0200 blanchet added theory to provide workaround to support nested datatypes in quickcheck (until quickcheck is generalized to support it with new datatypes)
Tue, 09 Aug 2016 21:18:32 +0200 nipkow New theory Balance_List
Mon, 08 Aug 2016 14:13:14 +0200 hoelzl rename HOL-Multivariate_Analysis to HOL-Analysis.
Thu, 04 Aug 2016 19:36:31 +0200 hoelzl HOL-Multivariate_Analysis: rename theories for more descriptive names
Sat, 23 Jul 2016 13:25:44 +0200 nipkow added new vcg based on existentially quantified while-rule
Fri, 22 Jul 2016 17:35:54 +0200 eberlm Removed redundant material related to primes
less more (0) -300 -100 -60 tip