src/HOL/Library/Library.thy
Sat, 06 Sep 2014 20:12:34 +0200 haftmann theory about lexicographic ordering on functions
Mon, 01 Sep 2014 16:17:46 +0200 blanchet took out legacy material from 'HOL/Library/Library.thy'
Thu, 28 Aug 2014 00:40:38 +0200 blanchet renaming theory 'Old_SMT'
Thu, 28 Aug 2014 00:40:37 +0200 blanchet moved old 'smt' method out of 'Main'
Tue, 19 Aug 2014 15:19:16 +0200 Andreas Lochbihler rename Quickcheck_Types to Lattice_Constructions and remove quickcheck setup
Thu, 12 Jun 2014 21:23:28 +0200 nipkow new theory of binary trees
Thu, 29 May 2014 16:13:47 +0200 nipkow removed Kleene_Algebra because of superior AFP entry; authors agreed
Tue, 20 May 2014 19:24:39 +0200 hoelzl add various lemmas
Tue, 13 May 2014 09:21:22 +0200 traytel bnf_decl -> bnf_axiomatization
Sat, 05 Apr 2014 10:01:07 +0200 haftmann proper inclusion into library
Mon, 10 Mar 2014 20:04:40 +0100 hoelzl introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
Wed, 29 Jan 2014 12:51:37 +0000 paulson Replacing the theory Library/Binomial by Number_Theory/Binomial
Fri, 24 Jan 2014 11:51:45 +0100 blanchet killed 'More_BNFs' by moving its various bits where they (now) belong
Mon, 20 Jan 2014 18:24:56 +0100 blanchet dissolved BNF session
Thu, 16 Jan 2014 16:33:19 +0100 blanchet moved 'Zorn' into 'Main', since it's a BNF dependency
Thu, 16 Jan 2014 16:20:17 +0100 blanchet adapted to move of Wfrec
Tue, 26 Nov 2013 12:29:31 +0100 hoelzl Add Zorn to HOL-Library
Wed, 20 Nov 2013 23:14:06 +0100 blanchet effectively reverted d25fc4c0ff62, to avoid quasi-cyclic dependencies with HOL-Cardinals and minimize BNF dependencies
Thu, 31 Oct 2013 11:44:20 +0100 haftmann more convenient place for a theory in solitariness
Thu, 31 Oct 2013 11:44:20 +0100 haftmann consolidated clone theory
Fri, 27 Sep 2013 14:43:26 +0200 kuncar new theory of finite sets as a subtype
Mon, 27 May 2013 22:32:28 +0200 wenzelm actually test theory Order_Union;
Tue, 09 Apr 2013 14:04:47 +0200 hoelzl move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
Tue, 26 Mar 2013 20:02:02 +0100 wenzelm tuned imports;
Sat, 09 Mar 2013 11:56:01 +0100 haftmann discontinued theory src/HOL/Library/Eval_Witness -- assumptions do not longer hold in presence of abstract types
Tue, 05 Mar 2013 15:26:57 +0100 nipkow New theory of infinity-extended types; should replace Extended_xyz eventually
Sun, 24 Feb 2013 20:29:13 +0100 haftmann turned example into library for comparing growth of functions
Sun, 17 Feb 2013 22:56:54 +0100 haftmann fundamentals about discrete logarithm and square root
Fri, 15 Feb 2013 11:47:34 +0100 haftmann attempt to re-establish conventions which theories are loaded into the grand unified library theory;
Tue, 20 Nov 2012 18:59:35 +0100 hoelzl add Countable_Set theory
Thu, 15 Nov 2012 10:49:58 +0100 immler regularity of measures, therefore:
Thu, 09 Aug 2012 14:09:36 +0200 wenzelm explicit FIXME;
Tue, 31 Jul 2012 13:55:39 +0200 kuncar implementation of sets by RBT trees for the code generator
Sun, 22 Jul 2012 09:56:34 +0200 haftmann library theories for debugging and parallel computing using code generation towards Isabelle/ML
Tue, 17 Jul 2012 23:11:27 +0200 haftmann explicitly import Dlist theory into library
Thu, 05 Jul 2012 13:24:09 +0200 haftmann Stub theory for division on functionals.
Tue, 29 May 2012 15:31:58 +0200 Andreas Lochbihler move FinFuns from AFP to repository
Fri, 30 Mar 2012 18:56:02 +0200 haftmann dropped now obsolete Cset theories
Mon, 26 Dec 2011 22:17:10 +0100 haftmann incorporated More_Set and More_List into the Main body -- to be consolidated later
Sun, 04 Dec 2011 13:10:19 +0100 huffman remove Library/Diagonalize.thy, because Library/Nat_Bijection.thy includes all the same functionality
Sun, 25 Sep 2011 09:37:33 +0200 haftmann Quotient_Set.thy is part of library
Mon, 12 Sep 2011 10:57:58 +0200 bulwahn moving connection of association lists to Mappings into a separate theory
Wed, 07 Sep 2011 23:38:52 +0200 haftmann theory of saturated naturals contributed by Peter Gammie
Sun, 28 Aug 2011 08:13:30 +0200 haftmann avoid loading List_Cset and Dlist_Cet at the same time
Wed, 17 Aug 2011 13:14:20 +0200 wenzelm moved theory Nested_Environment to HOL-Unix (a bit too specific for HOL-Library);
Tue, 16 Aug 2011 07:06:54 -0700 huffman get Library/Permutations.thy compiled and working again
Tue, 02 Aug 2011 11:52:57 +0200 krauss moved recursion combinator to HOL/Library/Wfrec.thy -- it is so fundamental and well-known that it should survive recdef
Tue, 02 Aug 2011 10:36:50 +0200 krauss moved recdef package to HOL/Library/Old_Recdef.thy
Tue, 26 Jul 2011 10:49:34 +0200 Andreas Lochbihler Add theory for setting up monad syntax for Cset
Mon, 25 Jul 2011 10:43:14 +0200 bulwahn removing SML_Quickcheck
Tue, 19 Jul 2011 14:35:44 +0200 hoelzl rename Nat_Infinity (inat) to Extended_Nat (enat)
Tue, 07 Jun 2011 11:12:05 +0200 bulwahn splitting Cset into Cset and List_Cset
Thu, 02 Jun 2011 08:55:08 +0200 bulwahn splitting Dlist theory in Dlist and Dlist_Cset
Wed, 01 Jun 2011 09:10:13 +0200 bulwahn splitting RBT theory into RBT and RBT_Mapping
Sat, 08 Jan 2011 17:39:51 +0100 wenzelm renamed Sum_Of_Squares to Sum_of_Squares;
Mon, 22 Nov 2010 17:49:12 +0100 haftmann merged
Mon, 22 Nov 2010 17:46:51 +0100 haftmann replaced misleading Fset/fset name -- these do not stand for finite sets
Mon, 22 Nov 2010 11:34:56 +0100 bulwahn adding Enum to HOL-Main image and removing it from HOL-Library
Wed, 03 Nov 2010 12:20:33 +0100 haftmann moved theory Quicksort from Library/ to ex/
Fri, 20 Aug 2010 17:48:30 +0200 haftmann split and enriched theory SetsAndFunctions
less more (0) -100 -60 tip