| Thu, 19 Feb 2009 12:03:31 -0800 |
huffman |
add formalization of a type of integers mod 2 to Library
|
file |
diff |
annotate
|
| Thu, 19 Feb 2009 09:42:23 -0800 |
huffman |
new theory of real inner product spaces
|
file |
diff |
annotate
|
| Wed, 18 Feb 2009 20:14:45 -0800 |
huffman |
move Polynomial.thy to Library
|
file |
diff |
annotate
|
| Wed, 18 Feb 2009 19:51:39 -0800 |
huffman |
move FrechetDeriv.thy to Library
|
file |
diff |
annotate
|
| Wed, 18 Feb 2009 19:32:26 -0800 |
huffman |
split polynomial-related stuff from Deriv.thy into Library/Poly_Deriv.thy
|
file |
diff |
annotate
|
| Thu, 12 Feb 2009 18:14:43 +0100 |
nipkow |
Moved FTA into Lib and cleaned it up a little.
|
file |
diff |
annotate
|
| Mon, 09 Feb 2009 17:21:46 +0000 |
chaieb |
added Determinants to Library
|
file |
diff |
annotate
|
| Mon, 09 Feb 2009 17:09:18 +0000 |
chaieb |
added Euclidean_Space and Glbs to Library
|
file |
diff |
annotate
|
| Mon, 09 Feb 2009 11:15:13 +0000 |
chaieb |
Added HOL/Library/Finite_Cartesian_Product.thy to Library
|
file |
diff |
annotate
|
| Fri, 06 Feb 2009 15:15:32 +0100 |
haftmann |
session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
|
file |
diff |
annotate
|
| Fri, 06 Feb 2009 00:10:58 +0000 |
chaieb |
fixed Proofs and dependencies ; Theory Dense_Linear_Order moved to Library
|
file |
diff |
annotate
|
| Thu, 05 Feb 2009 14:14:02 +0100 |
haftmann |
moved Random.thy to Library
|
file |
diff |
annotate
|
| Mon, 02 Feb 2009 13:56:22 +0100 |
haftmann |
added Mapping.thy to Library
|
file |
diff |
annotate
|
| Thu, 29 Jan 2009 14:56:29 +0000 |
chaieb |
Added Formal_Power_Series in imports
|
file |
diff |
annotate
|
| Wed, 28 Jan 2009 11:04:10 +0100 |
haftmann |
Reflection.thy now in HOL/Library
|
file |
diff |
annotate
|
| Fri, 16 Jan 2009 08:28:53 +0100 |
haftmann |
moved Univ_Poly to Library
|
file |
diff |
annotate
|
| Thu, 08 Jan 2009 17:10:41 +0100 |
haftmann |
split of Imperative_HOL theories from HOL-Library
|
file |
diff |
annotate
|
| Mon, 29 Dec 2008 14:08:08 +0100 |
haftmann |
adapted HOL source structure to distribution layout
|
file |
diff |
annotate
|
| Wed, 10 Dec 2008 10:23:47 +0100 |
nipkow |
moved ContNotDenum into Library
|
file |
diff |
annotate
|
| Wed, 03 Dec 2008 15:58:44 +0100 |
haftmann |
made repository layout more coherent with logical distribution structure; stripped some $Id$s
|
file |
diff |
annotate
|
| Thu, 23 Oct 2008 00:24:31 +0200 |
wenzelm |
fixed and reactivated HOL/Library/Pocklington.thy -- by Mark Hillebrand;
|
file |
diff |
annotate
|
| Tue, 16 Sep 2008 09:21:24 +0200 |
haftmann |
evaluation using code generator
|
file |
diff |
annotate
|
| Tue, 02 Sep 2008 22:37:20 +0200 |
nipkow |
Replaced Library/NatPair by Nat_Int_Bij.
|
file |
diff |
annotate
|
| Fri, 18 Jul 2008 18:25:56 +0200 |
haftmann |
refined code generator setup for rational numbers; more simplification rules for rational numbers
|
file |
diff |
annotate
|
| 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)
|
file |
diff |
annotate
|
| Thu, 26 Jun 2008 10:07:01 +0200 |
haftmann |
established Plain theory and image
|
file |
diff |
annotate
|
| Fri, 20 Jun 2008 21:00:16 +0200 |
haftmann |
moved Float.thy to Library
|
file |
diff |
annotate
|
| Thu, 20 Mar 2008 12:01:10 +0100 |
haftmann |
added theory Library/Enum.thy
|
file |
diff |
annotate
|
| Fri, 14 Mar 2008 19:57:32 +0100 |
nipkow |
Added Order_Relation
|
file |
diff |
annotate
|
| Fri, 07 Mar 2008 13:53:01 +0100 |
haftmann |
canonical order on option type
|
file |
diff |
annotate
|
| Mon, 03 Mar 2008 14:03:19 +0100 |
krauss |
new theory of red-black trees, an efficient implementation of finite maps.
|
file |
diff |
annotate
|
| Thu, 28 Feb 2008 00:11:28 +0100 |
wenzelm |
renamed ListSpace to ListVector;
|
file |
diff |
annotate
|
| Wed, 27 Feb 2008 21:41:08 +0100 |
haftmann |
added theories for imperative HOL
|
file |
diff |
annotate
|
| Wed, 27 Feb 2008 14:39:51 +0100 |
chaieb |
Loads Dense_Linear_Order.thy
|
file |
diff |
annotate
|
| Mon, 25 Feb 2008 11:27:08 +0100 |
chaieb |
Uses Univ_Poly.thy
|
file |
diff |
annotate
|
| Mon, 14 Jan 2008 11:45:57 +0100 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| Tue, 06 Nov 2007 20:27:33 +0100 |
wenzelm |
removed dependencies on Size_Change_Termination from HOL-Library;
|
file |
diff |
annotate
|
| Fri, 12 Oct 2007 08:21:09 +0200 |
haftmann |
consolidated naming conventions for code generator theories
|
file |
diff |
annotate
|
| Tue, 18 Sep 2007 07:46:00 +0200 |
haftmann |
introduced generic concepts for theory interpretators
|
file |
diff |
annotate
|
| Tue, 18 Sep 2007 05:42:46 +0200 |
nipkow |
Added function package to PreList
|
file |
diff |
annotate
|
| Thu, 06 Sep 2007 11:32:28 +0200 |
berghofe |
Integrated Executable_Rat and Executable_Real theories into
|
file |
diff |
annotate
|
| Mon, 20 Aug 2007 00:22:18 +0200 |
kleing |
boolean algebras as locales and numbers as types by Brian Huffman
|
file |
diff |
annotate
|
| Wed, 15 Aug 2007 08:57:40 +0200 |
haftmann |
added Eval_Witness theory
|
file |
diff |
annotate
|
| Thu, 09 Aug 2007 15:52:49 +0200 |
haftmann |
proper implementation of rational numbers
|
file |
diff |
annotate
|
| Thu, 19 Jul 2007 21:47:39 +0200 |
haftmann |
uniform naming conventions for CG theories
|
file |
diff |
annotate
|
| Fri, 01 Jun 2007 22:09:16 +0200 |
nipkow |
Moved list comprehension into List
|
file |
diff |
annotate
|
| Fri, 25 May 2007 18:08:34 +0200 |
nipkow |
Added List_Comprehension
|
file |
diff |
annotate
|
| Tue, 15 May 2007 18:28:02 +0200 |
chaieb |
A verified theory for rational numbers representation and simple calculations;
|
file |
diff |
annotate
|
| Thu, 26 Apr 2007 13:32:59 +0200 |
haftmann |
moved code generation pretty integers and characters to separate theories
|
file |
diff |
annotate
|
| Mon, 26 Mar 2007 14:53:02 +0200 |
haftmann |
importing Eval theory
|
file |
diff |
annotate
|
| Mon, 26 Feb 2007 21:34:16 +0100 |
krauss |
Added formalization of size-change principle (experimental).
|
file |
diff |
annotate
|
| Mon, 04 Dec 2006 15:15:59 +0100 |
krauss |
added Ramsey.thy to Library imports, to include it in the daily builds
|
file |
diff |
annotate
|
| Wed, 08 Nov 2006 23:11:13 +0100 |
wenzelm |
moved theories Parity, GCD, Binomial to Library;
|
file |
diff |
annotate
|
| Mon, 06 Nov 2006 16:28:33 +0100 |
haftmann |
added state monad to HOL library
|
file |
diff |
annotate
|
| Sun, 01 Oct 2006 18:29:26 +0200 |
wenzelm |
moved theory Infinite_Set to Library;
|
file |
diff |
annotate
|
| Mon, 21 Aug 2006 11:02:39 +0200 |
haftmann |
added some codegen examples/applications
|
file |
diff |
annotate
|
| Tue, 09 May 2006 10:13:09 +0200 |
haftmann |
added ExecutableRat.thy
|
file |
diff |
annotate
|
| Fri, 05 May 2006 17:17:21 +0200 |
krauss |
First usable version of the new function definition package (HOL/function_packake/...).
|
file |
diff |
annotate
|
| Wed, 26 Apr 2006 07:01:33 +0200 |
kleing |
moved arithmetic series to geometric series in SetInterval
|
file |
diff |
annotate
|
| Fri, 07 Apr 2006 03:20:34 +0200 |
kleing |
renamed ASeries to Arithmetic_Series, removed the ^M
|
file |
diff |
annotate
|