| Fri, 02 Apr 2004 17:37:45 +0200 |
skalberg |
Added HOL proof importer.
|
file |
diff |
annotate
|
| Fri, 02 Apr 2004 17:36:01 +0200 |
webertj |
Tools/sat_solver.ML and Tools/prop_logic.ML added
|
file |
diff |
annotate
|
| Thu, 01 Apr 2004 15:05:04 +0200 |
paulson |
removal of Binary Trees examples prepratory to its going into AFP
|
file |
diff |
annotate
|
| Wed, 31 Mar 2004 11:02:00 +0200 |
nipkow |
Lex now in AFP
|
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
|
| Thu, 25 Mar 2004 05:37:32 +0100 |
kleing |
moved MiniML and AVL to archive of formal proofs
|
file |
diff |
annotate
|
| Fri, 19 Mar 2004 10:51:03 +0100 |
paulson |
conversion of Hyperreal/Lim to new-style
|
file |
diff |
annotate
|
| Mon, 08 Mar 2004 11:11:58 +0100 |
paulson |
new theory of infinite sets
|
file |
diff |
annotate
|
| Sat, 06 Mar 2004 19:32:21 +0100 |
nipkow |
Lex: removed last ML files
|
file |
diff |
annotate
|
| Fri, 05 Mar 2004 15:18:59 +0100 |
paulson |
Conversion of Poly to Isar script, and other tidying of HOL/Hyperreal
|
file |
diff |
annotate
|
| Thu, 04 Mar 2004 15:49:42 +0100 |
nipkow |
Lex: ML -> thy
|
file |
diff |
annotate
|
| Thu, 04 Mar 2004 12:06:07 +0100 |
paulson |
new material from Avigad, and simplified treatment of division by 0
|
file |
diff |
annotate
|
| Thu, 04 Mar 2004 10:06:13 +0100 |
nipkow |
Removed ML files from Lex
|
file |
diff |
annotate
|
| Tue, 02 Mar 2004 11:05:55 +0100 |
paulson |
converted Hyperreal/IntFloor to Isar script
|
file |
diff |
annotate
|
| Tue, 02 Mar 2004 01:34:54 +0100 |
kleing |
converted MiniML to Isar
|
file |
diff |
annotate
|
| Mon, 01 Mar 2004 11:52:59 +0100 |
paulson |
converted Hyperreal/HTranscendental to Isar script
|
file |
diff |
annotate
|
| Mon, 01 Mar 2004 05:39:32 +0100 |
kleing |
converted to Isar
|
file |
diff |
annotate
|
| Thu, 26 Feb 2004 17:08:23 +0100 |
paulson |
converted Hyperreal/Series to Isar script
|
file |
diff |
annotate
|
| Thu, 26 Feb 2004 11:31:36 +0100 |
paulson |
converted Hyperreal/NatStar to Isar script
|
file |
diff |
annotate
|
| Wed, 25 Feb 2004 16:22:36 +0100 |
paulson |
converted Hyperreal/HSeries to Isar script
|
file |
diff |
annotate
|
| Tue, 24 Feb 2004 16:38:51 +0100 |
paulson |
converted Hyperreal/Log and Hyperreal/HLog to Isar scripts
|
file |
diff |
annotate
|
| Mon, 23 Feb 2004 17:33:38 +0100 |
paulson |
converted HOL/Complex/NSInduct to Isar script
|
file |
diff |
annotate
|
| Mon, 23 Feb 2004 16:35:46 +0100 |
paulson |
converted HOL/Complex/NSCA to Isar script
|
file |
diff |
annotate
|
| Sat, 21 Feb 2004 20:05:16 +0100 |
paulson |
conversion of Complex/CStar to Isar script
|
file |
diff |
annotate
|
| Sat, 21 Feb 2004 15:54:32 +0100 |
paulson |
conversion of Complex/CSeries to Isar script
|
file |
diff |
annotate
|
| Sat, 21 Feb 2004 11:43:39 +0100 |
paulson |
conversion of Complex/CLim to Isar script
|
file |
diff |
annotate
|
| Thu, 19 Feb 2004 15:57:34 +0100 |
ballarin |
Efficient, graph-based reasoner for linear and partial orders.
|
file |
diff |
annotate
|
| Sun, 15 Feb 2004 10:46:37 +0100 |
paulson |
Polymorphic treatment of binary arithmetic using axclasses
|
file |
diff |
annotate
|
| Tue, 10 Feb 2004 12:02:11 +0100 |
paulson |
generic of_nat and of_int functions, and generalization of iszero
|
file |
diff |
annotate
|
| Tue, 03 Feb 2004 11:06:36 +0100 |
paulson |
tidying of the complex numbers
|
file |
diff |
annotate
|
| Mon, 02 Feb 2004 12:23:46 +0100 |
paulson |
Conversion of HyperNat to Isar format and its declaration as a semiring
|
file |
diff |
annotate
|
| Thu, 29 Jan 2004 16:51:17 +0100 |
paulson |
simplifications in the hyperreals
|
file |
diff |
annotate
|
| Wed, 28 Jan 2004 17:01:01 +0100 |
paulson |
tidying up arithmetic for the hyperreals
|
file |
diff |
annotate
|
| Wed, 28 Jan 2004 10:41:49 +0100 |
paulson |
converted Real/Lubs to Isar script. Converting arithmetic setup
|
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
|
| Wed, 14 Jan 2004 00:13:04 +0100 |
nipkow |
Told linear arithmetic package about injections "real" from nat/int into real.
|
file |
diff |
annotate
|
| Mon, 12 Jan 2004 16:51:45 +0100 |
paulson |
Added lemmas to Ring_and_Field with slightly modified simplification rules
|
file |
diff |
annotate
|
| Sat, 10 Jan 2004 13:35:10 +0100 |
webertj |
Adding 'refute' to HOL.
|
file |
diff |
annotate
|
| Fri, 09 Jan 2004 10:46:18 +0100 |
paulson |
Defining the type class "ringpower" and deleting superseded theorems for
|
file |
diff |
annotate
|
| Thu, 01 Jan 2004 21:47:07 +0100 |
paulson |
conversion of Real/PReal to Isar script;
|
file |
diff |
annotate
|
| Thu, 01 Jan 2004 10:06:32 +0100 |
paulson |
tweaking of lemmas in RealDef, RealOrd
|
file |
diff |
annotate
|
| Tue, 23 Dec 2003 17:41:52 +0100 |
paulson |
converting Hyperreal/NthRoot to Isar
|
file |
diff |
annotate
|
| Tue, 23 Dec 2003 16:53:33 +0100 |
paulson |
converting Complex/Complex.ML to Isar
|
file |
diff |
annotate
|
| Tue, 23 Dec 2003 14:45:47 +0100 |
paulson |
tidying up hcomplex arithmetic
|
file |
diff |
annotate
|
| Mon, 22 Dec 2003 18:29:20 +0100 |
paulson |
converted Complex/NSComplex to Isar script
|
file |
diff |
annotate
|
| Mon, 22 Dec 2003 12:50:22 +0100 |
paulson |
moving HyperArith0.ML to other theories
|
file |
diff |
annotate
|
| Wed, 17 Dec 2003 16:23:52 +0100 |
paulson |
converted Hyperreal/HyperDef to Isar script
|
file |
diff |
annotate
|
| Tue, 16 Dec 2003 15:38:09 +0100 |
paulson |
converted Hyperreal/HyperOrd to new-style theory
|
file |
diff |
annotate
|
| Wed, 10 Dec 2003 16:47:50 +0100 |
paulson |
combining Real/{RealArith0,real_arith}.ML
|
file |
diff |
annotate
|
| Wed, 10 Dec 2003 15:59:34 +0100 |
paulson |
Moving some theorems from Real/RealArith0.ML
|
file |
diff |
annotate
|
| Thu, 04 Dec 2003 16:16:36 +0100 |
paulson |
further simplifications of the integer development; converting more .ML files
|
file |
diff |
annotate
|
| Thu, 04 Dec 2003 10:29:17 +0100 |
paulson |
Tidying of the integer development; towards removing the
|
file |
diff |
annotate
|
| Fri, 28 Nov 2003 12:09:37 +0100 |
paulson |
conversion of some Real theories to Isar scripts
|
file |
diff |
annotate
|
| Thu, 27 Nov 2003 10:47:55 +0100 |
paulson |
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
|
file |
diff |
annotate
|
| Tue, 25 Nov 2003 10:37:03 +0100 |
paulson |
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
|
file |
diff |
annotate
|
| Mon, 24 Nov 2003 15:33:07 +0100 |
paulson |
conversion of integers to use Ring_and_Field;
|
file |
diff |
annotate
|
| Fri, 21 Nov 2003 11:15:40 +0100 |
paulson |
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
|
file |
diff |
annotate
|
| Thu, 20 Nov 2003 10:42:00 +0100 |
paulson |
conversion of Integ/Int_lemmas.ML to Isar script
|
file |
diff |
annotate
|
| Tue, 18 Nov 2003 11:01:52 +0100 |
paulson |
conversion of ML to Isar scripts
|
file |
diff |
annotate
|
| Wed, 22 Oct 2003 10:52:36 +0200 |
paulson |
InductiveInvariant_examples illustrates advanced recursive function definitions
|
file |
diff |
annotate
|