Fri, 02 Jul 2010 14:23:17 +0200 |
remove codegeneration-related theories from big library theory
|
file | diff | annotate |
Thu, 01 Jul 2010 11:48:42 +0200 |
Add theory for indicator function.
|
file | diff | annotate |
Thu, 20 May 2010 16:35:54 +0200 |
added theory More_List
|
file | diff | annotate |
Mon, 17 May 2010 10:58:31 +0200 |
dropped old Library/Word.thy and toy example ex/Adder.thy
|
file | diff | annotate |
Tue, 04 May 2010 18:05:22 +0200 |
Add Convex to Library build
|
file | diff | annotate |
Thu, 15 Apr 2010 12:27:14 +0200 |
theory RBT with abstract type of red-black trees backed by implementation RBT_Impl
|
file | diff | annotate |
Sat, 13 Mar 2010 17:19:12 +0100 |
removed obsolete HOL/Library/Coinductive_List.thy, superceded by thys/Coinductive/Coinductive_List.thy in AFP/f2f5727b77d0;
|
file | diff | annotate |
Sat, 06 Mar 2010 15:31:30 +0100 |
added Table.thy
|
file | diff | annotate |
Mon, 22 Feb 2010 15:53:18 +0100 |
added Dlist
|
file | diff | annotate |
Fri, 19 Feb 2010 13:54:19 +0100 |
Initial version of HOL quotient package.
|
file | diff | annotate |
Wed, 10 Feb 2010 19:37:34 +0100 |
renamed Library/Quotient.thy to Library/Quotient_Type.thy to avoid clash with new theory Quotient in Main HOL;
|
file | diff | annotate |
Wed, 10 Feb 2010 14:12:02 +0100 |
revert uninspired Structure_Syntax experiment
|
file | diff | annotate |
Mon, 08 Feb 2010 14:08:32 +0100 |
merged
|
file | diff | annotate |
Mon, 08 Feb 2010 14:06:41 +0100 |
separate library theory for type classes combining lattices with various algebraic structures
|
file | diff | annotate |
Mon, 08 Feb 2010 10:36:02 +0100 |
separate theory for index structures
|
file | diff | annotate |
Mon, 07 Dec 2009 14:54:01 +0100 |
merged Crude_Executable_Set into Executable_Set
|
file | diff | annotate |
Wed, 02 Dec 2009 17:53:34 +0100 |
added Crude_Executable_Set.thy
|
file | diff | annotate |
Thu, 12 Nov 2009 20:38:57 +0100 |
added a tabled implementation of the reflexive transitive closure
|
file | diff | annotate |
Fri, 30 Oct 2009 13:59:49 +0100 |
moved Commutative_Ring into session Decision_Procs
|
file | diff | annotate |
Mon, 26 Oct 2009 11:19:24 +0100 |
re-moved theory Fin_Fun to AFP
|
file | diff | annotate |
Mon, 26 Oct 2009 09:03:57 +0100 |
merged
|
file | diff | annotate |
Fri, 23 Oct 2009 13:23:18 +0200 |
distinguished session for multivariate analysis
|
file | diff | annotate |
Fri, 23 Oct 2009 17:12:36 +0200 |
turned off old quickcheck
|
file | diff | annotate |
Tue, 01 Sep 2009 15:39:33 +0200 |
some reorganization of number theory
|
file | diff | annotate |
Fri, 10 Jul 2009 09:24:50 +0200 |
move Kleene_Algebra to Library
|
file | diff | annotate |
Mon, 29 Jun 2009 12:18:55 +0200 |
renamed theory Code_Set to Fset
|
file | diff | annotate |
Thu, 25 Jun 2009 17:07:18 +0200 |
added List_Set and Code_Set theories
|
file | diff | annotate |
Tue, 23 Jun 2009 10:22:11 +0200 |
Added Library/Fraction_Field.thy: The fraction field of any integral
|
file | diff | annotate |
Tue, 02 Jun 2009 15:53:34 +0200 |
added Fin_Fun theory
|
file | diff | annotate |
Tue, 02 Jun 2009 10:00:29 +0200 |
Added Convex_Euclidean_Space.thy again.
|
file | diff | annotate |
Thu, 28 May 2009 18:59:51 +0200 |
Removed Convex_Euclidean_Space.thy from Library.
|
file | diff | annotate |
Thu, 28 May 2009 13:56:50 +0200 |
Added Convex_Euclidean_Space to Library.thy and Library/IsaMakefile
|
file | diff | annotate |
Sat, 16 May 2009 20:16:49 +0200 |
experimental move of Quickcheck and related theories to HOL image
|
file | diff | annotate |
Tue, 12 May 2009 17:32:49 +0100 |
Added files Sum_Of_Squares.thy, positivstellensatz.ML and sum_of_squares.ML to Library
|
file | diff | annotate |
Thu, 07 May 2009 12:17:17 +0200 |
added theory for explicit equivalence relation in preorders
|
file | diff | annotate |
Fri, 06 Mar 2009 20:30:16 +0100 |
constructive version of Cantor's first diagonalization argument
|
file | diff | annotate |
Wed, 04 Mar 2009 19:21:55 +0000 |
Added Libray dependency on Topology_Euclidean_Space
|
file | diff | annotate |
Wed, 04 Mar 2009 11:05:29 +0100 |
Merge.
|
file | diff | annotate |
Wed, 04 Mar 2009 10:45:52 +0100 |
Merge.
|
file | diff | annotate |
Fri, 20 Feb 2009 08:02:11 -0800 |
add theory of products as real vector spaces to Library
|
file | diff | annotate |
Fri, 20 Feb 2009 07:41:41 -0800 |
add new theory Product_plus.thy to Library
|
file | diff | annotate |
Thu, 19 Feb 2009 12:03:31 -0800 |
add formalization of a type of integers mod 2 to Library
|
file | diff | annotate |
Thu, 19 Feb 2009 09:42:23 -0800 |
new theory of real inner product spaces
|
file | diff | annotate |
Wed, 18 Feb 2009 20:14:45 -0800 |
move Polynomial.thy to Library
|
file | diff | annotate |
Wed, 18 Feb 2009 19:51:39 -0800 |
move FrechetDeriv.thy to Library
|
file | diff | annotate |
Wed, 18 Feb 2009 19:32:26 -0800 |
split polynomial-related stuff from Deriv.thy into Library/Poly_Deriv.thy
|
file | diff | annotate |
Thu, 12 Feb 2009 18:14:43 +0100 |
Moved FTA into Lib and cleaned it up a little.
|
file | diff | annotate |
Mon, 09 Feb 2009 17:21:46 +0000 |
added Determinants to Library
|
file | diff | annotate |
Mon, 09 Feb 2009 17:09:18 +0000 |
added Euclidean_Space and Glbs to Library
|
file | diff | annotate |
Mon, 09 Feb 2009 11:15:13 +0000 |
Added HOL/Library/Finite_Cartesian_Product.thy to Library
|
file | diff | annotate |
Fri, 06 Feb 2009 15:15:32 +0100 |
session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
|
file | diff | annotate |
Fri, 06 Feb 2009 00:10:58 +0000 |
fixed Proofs and dependencies ; Theory Dense_Linear_Order moved to Library
|
file | diff | annotate |
Thu, 05 Feb 2009 14:14:02 +0100 |
moved Random.thy to Library
|
file | diff | annotate |
Mon, 02 Feb 2009 13:56:22 +0100 |
added Mapping.thy to Library
|
file | diff | annotate |
Thu, 29 Jan 2009 14:56:29 +0000 |
Added Formal_Power_Series in imports
|
file | diff | annotate |
Wed, 28 Jan 2009 11:04:10 +0100 |
Reflection.thy now in HOL/Library
|
file | diff | annotate |
Fri, 16 Jan 2009 08:28:53 +0100 |
moved Univ_Poly to Library
|
file | diff | annotate |
Thu, 08 Jan 2009 17:10:41 +0100 |
split of Imperative_HOL theories from HOL-Library
|
file | diff | annotate |
Mon, 29 Dec 2008 14:08:08 +0100 |
adapted HOL source structure to distribution layout
|
file | diff | annotate |
Wed, 10 Dec 2008 10:23:47 +0100 |
moved ContNotDenum into Library
|
file | diff | annotate |