| 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
|
| Fri, 10 Mar 2006 16:05:34 +0100 |
schirmer |
Added Library/AssocList.thy
|
file |
diff |
annotate
|
| Sun, 19 Feb 2006 13:21:32 +0100 |
kleing |
* added Library/ASeries (sum of arithmetic series with instantiation to nat and int)
|
file |
diff |
annotate
|
| Tue, 13 Dec 2005 19:32:04 +0100 |
wenzelm |
added HOL/Library/Coinductive_List.thy;
|
file |
diff |
annotate
|
| Sun, 25 Sep 2005 20:12:59 +0200 |
berghofe |
Added ExecutableSet.
|
file |
diff |
annotate
|
| Tue, 20 Sep 2005 14:10:29 +0200 |
wenzelm |
added Commutative_Ring (from Main HOL);
|
file |
diff |
annotate
|
| Mon, 01 Aug 2005 11:39:33 +0200 |
obua |
1. changed configuration variables for linear programming (Cplex_tools):
|
file |
diff |
annotate
|
| Mon, 25 Jul 2005 18:54:49 +0200 |
avigad |
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
|
file |
diff |
annotate
|
| Sun, 29 May 2005 12:41:40 +0200 |
obua |
Removes an inconsistent definition from Library.thy ,
|
file |
diff |
annotate
|
| Thu, 14 Apr 2005 17:57:04 +0200 |
nipkow |
Removed dir Orderings in Library
|
file |
diff |
annotate
|
| Wed, 26 Jan 2005 16:39:44 +0100 |
nipkow |
added OptionalSugar
|
file |
diff |
annotate
|
| Wed, 24 Nov 2004 10:30:19 +0100 |
berghofe |
Added EfficientNat
|
file |
diff |
annotate
|
| Wed, 18 Aug 2004 11:09:40 +0200 |
nipkow |
import -> imports
|
file |
diff |
annotate
|
| Mon, 16 Aug 2004 14:22:27 +0200 |
nipkow |
New theory header syntax.
|
file |
diff |
annotate
|
| Thu, 06 May 2004 14:14:18 +0200 |
wenzelm |
tuned document;
|
file |
diff |
annotate
|
| Mon, 29 Mar 2004 15:35:04 +0200 |
skalberg |
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
|
file |
diff |
annotate
|
| Tue, 27 Jan 2004 15:39:51 +0100 |
paulson |
replacing HOL/Real/PRat, PNat by the rational number development
|
file |
diff |
annotate
|
| Mon, 24 Nov 2003 15:33:07 +0100 |
paulson |
conversion of integers to use Ring_and_Field;
|
file |
diff |
annotate
|
| Thu, 24 Jul 2003 16:37:04 +0200 |
paulson |
new theory NatPair of the injection from nat*nat -> nat
|
file |
diff |
annotate
|
| Sat, 09 Jun 2001 14:18:19 +0200 |
wenzelm |
tuned Primes theory;
|
file |
diff |
annotate
|
| Thu, 31 May 2001 16:52:54 +0200 |
oheimb |
added Library/Nat_Infinity.thy and Library/Continuity.thy
|
file |
diff |
annotate
|
| Sun, 04 Feb 2001 19:43:15 +0100 |
wenzelm |
added Permutation;
|
file |
diff |
annotate
|
| Fri, 26 Jan 2001 15:50:52 +0100 |
nipkow |
Merged Example into While_Combi
|
file |
diff |
annotate
|
| Sat, 20 Jan 2001 00:35:10 +0100 |
wenzelm |
Ring_and_Field_Example;
|
file |
diff |
annotate
|
| Fri, 19 Jan 2001 23:53:07 +0100 |
wenzelm |
added HOL/Library/Nested_Environment.thy;
|
file |
diff |
annotate
|
| Wed, 06 Dec 2000 21:52:49 +0100 |
wenzelm |
activate Rational_Numbers;
|
file |
diff |
annotate
|
| Wed, 06 Dec 2000 21:32:25 +0100 |
wenzelm |
deactivate Rational_Numbers (tmp!);
|
file |
diff |
annotate
|
| Wed, 06 Dec 2000 20:45:36 +0100 |
wenzelm |
Rational_Numbers;
|
file |
diff |
annotate
|
| Fri, 17 Nov 2000 18:47:33 +0100 |
wenzelm |
Ring_and_Field;
|
file |
diff |
annotate
|
| Wed, 25 Oct 2000 18:32:40 +0200 |
wenzelm |
added List_Prefix;
|
file |
diff |
annotate
|
| Wed, 18 Oct 2000 23:31:16 +0200 |
wenzelm |
"The Supplemental Isabelle/HOL Library";
|
file |
diff |
annotate
|