src/HOL/Library/Library.thy
Tue, 23 Jun 2009 10:22:11 +0200 chaieb Added Library/Fraction_Field.thy: The fraction field of any integral
Tue, 02 Jun 2009 15:53:34 +0200 haftmann added Fin_Fun theory
Tue, 02 Jun 2009 10:00:29 +0200 berghofe Added Convex_Euclidean_Space.thy again.
Thu, 28 May 2009 18:59:51 +0200 himmelma Removed Convex_Euclidean_Space.thy from Library.
Thu, 28 May 2009 13:56:50 +0200 himmelma Added Convex_Euclidean_Space to Library.thy and Library/IsaMakefile
Sat, 16 May 2009 20:16:49 +0200 haftmann experimental move of Quickcheck and related theories to HOL image
Tue, 12 May 2009 17:32:49 +0100 chaieb Added files Sum_Of_Squares.thy, positivstellensatz.ML and sum_of_squares.ML to Library
Thu, 07 May 2009 12:17:17 +0200 haftmann added theory for explicit equivalence relation in preorders
Fri, 06 Mar 2009 20:30:16 +0100 haftmann constructive version of Cantor's first diagonalization argument
Wed, 04 Mar 2009 19:21:55 +0000 chaieb Added Libray dependency on Topology_Euclidean_Space
Wed, 04 Mar 2009 11:05:29 +0100 blanchet Merge.
Wed, 04 Mar 2009 10:45:52 +0100 blanchet Merge.
Fri, 20 Feb 2009 08:02:11 -0800 huffman add theory of products as real vector spaces to Library
Fri, 20 Feb 2009 07:41:41 -0800 huffman add new theory Product_plus.thy to Library
Thu, 19 Feb 2009 12:03:31 -0800 huffman add formalization of a type of integers mod 2 to Library
Thu, 19 Feb 2009 09:42:23 -0800 huffman new theory of real inner product spaces
Wed, 18 Feb 2009 20:14:45 -0800 huffman move Polynomial.thy to Library
Wed, 18 Feb 2009 19:51:39 -0800 huffman move FrechetDeriv.thy to Library
Wed, 18 Feb 2009 19:32:26 -0800 huffman split polynomial-related stuff from Deriv.thy into Library/Poly_Deriv.thy
Thu, 12 Feb 2009 18:14:43 +0100 nipkow Moved FTA into Lib and cleaned it up a little.
Mon, 09 Feb 2009 17:21:46 +0000 chaieb added Determinants to Library
Mon, 09 Feb 2009 17:09:18 +0000 chaieb added Euclidean_Space and Glbs to Library
Mon, 09 Feb 2009 11:15:13 +0000 chaieb Added HOL/Library/Finite_Cartesian_Product.thy to Library
Fri, 06 Feb 2009 15:15:32 +0100 haftmann session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
Fri, 06 Feb 2009 00:10:58 +0000 chaieb fixed Proofs and dependencies ; Theory Dense_Linear_Order moved to Library
Thu, 05 Feb 2009 14:14:02 +0100 haftmann moved Random.thy to Library
Mon, 02 Feb 2009 13:56:22 +0100 haftmann added Mapping.thy to Library
Thu, 29 Jan 2009 14:56:29 +0000 chaieb Added Formal_Power_Series in imports
Wed, 28 Jan 2009 11:04:10 +0100 haftmann Reflection.thy now in HOL/Library
Fri, 16 Jan 2009 08:28:53 +0100 haftmann moved Univ_Poly to Library
Thu, 08 Jan 2009 17:10:41 +0100 haftmann split of Imperative_HOL theories from HOL-Library
Mon, 29 Dec 2008 14:08:08 +0100 haftmann adapted HOL source structure to distribution layout
Wed, 10 Dec 2008 10:23:47 +0100 nipkow moved ContNotDenum into Library
Wed, 03 Dec 2008 15:58:44 +0100 haftmann made repository layout more coherent with logical distribution structure; stripped some $Id$s
Thu, 23 Oct 2008 00:24:31 +0200 wenzelm fixed and reactivated HOL/Library/Pocklington.thy -- by Mark Hillebrand;
Tue, 16 Sep 2008 09:21:24 +0200 haftmann evaluation using code generator
Tue, 02 Sep 2008 22:37:20 +0200 nipkow Replaced Library/NatPair by Nat_Int_Bij.
Fri, 18 Jul 2008 18:25:56 +0200 haftmann refined code generator setup for rational numbers; more simplification rules for rational numbers
Thu, 03 Jul 2008 18:16:40 +0200 huffman add Infinite_Set and Zorn back in (since they are no longer included in main HOL image)
Thu, 26 Jun 2008 10:07:01 +0200 haftmann established Plain theory and image
Fri, 20 Jun 2008 21:00:16 +0200 haftmann moved Float.thy to Library
Thu, 20 Mar 2008 12:01:10 +0100 haftmann added theory Library/Enum.thy
Fri, 14 Mar 2008 19:57:32 +0100 nipkow Added Order_Relation
Fri, 07 Mar 2008 13:53:01 +0100 haftmann canonical order on option type
Mon, 03 Mar 2008 14:03:19 +0100 krauss new theory of red-black trees, an efficient implementation of finite maps.
Thu, 28 Feb 2008 00:11:28 +0100 wenzelm renamed ListSpace to ListVector;
Wed, 27 Feb 2008 21:41:08 +0100 haftmann added theories for imperative HOL
Wed, 27 Feb 2008 14:39:51 +0100 chaieb Loads Dense_Linear_Order.thy
Mon, 25 Feb 2008 11:27:08 +0100 chaieb Uses Univ_Poly.thy
Mon, 14 Jan 2008 11:45:57 +0100 nipkow *** empty log message ***
Tue, 06 Nov 2007 20:27:33 +0100 wenzelm removed dependencies on Size_Change_Termination from HOL-Library;
Fri, 12 Oct 2007 08:21:09 +0200 haftmann consolidated naming conventions for code generator theories
Tue, 18 Sep 2007 07:46:00 +0200 haftmann introduced generic concepts for theory interpretators
Tue, 18 Sep 2007 05:42:46 +0200 nipkow Added function package to PreList
Thu, 06 Sep 2007 11:32:28 +0200 berghofe Integrated Executable_Rat and Executable_Real theories into
Mon, 20 Aug 2007 00:22:18 +0200 kleing boolean algebras as locales and numbers as types by Brian Huffman
Wed, 15 Aug 2007 08:57:40 +0200 haftmann added Eval_Witness theory
Thu, 09 Aug 2007 15:52:49 +0200 haftmann proper implementation of rational numbers
Thu, 19 Jul 2007 21:47:39 +0200 haftmann uniform naming conventions for CG theories
Fri, 01 Jun 2007 22:09:16 +0200 nipkow Moved list comprehension into List
less more (0) -100 -60 tip