| Thu, 02 Sep 2004 16:52:21 +0200 |
new example of a quotiented nested data type
|
file | diff | annotate |
| Fri, 20 Aug 2004 12:20:09 +0200 |
fix to eliminate excessive case-splits in the recursion equations, by Luca Dixon
|
file | diff | annotate |
| Tue, 03 Aug 2004 14:47:51 +0200 |
New transitivity reasoners for transitivity only and quasi orders.
|
file | diff | annotate |
| Sat, 31 Jul 2004 20:54:23 +0200 |
conversion of Hyperreal/{Fact,Filter} to Isar scripts
|
file | diff | annotate |
| Fri, 30 Jul 2004 18:37:58 +0200 |
conversion of Integration and NSPrimes to Isar scripts
|
file | diff | annotate |
| Wed, 28 Jul 2004 16:26:27 +0200 |
conversion of SEQ.ML to Isar script
|
file | diff | annotate |
| Wed, 28 Jul 2004 10:49:29 +0200 |
conversion of Hyperreal/MacLaurin_lemmas to Isar script
|
file | diff | annotate |
| Mon, 26 Jul 2004 17:34:52 +0200 |
converting Hyperreal/Transcendental to Isar script
|
file | diff | annotate |
| Mon, 26 Jul 2004 15:48:50 +0200 |
New prover for transitive and reflexive-transitive closure of relations.
|
file | diff | annotate |
| Fri, 16 Jul 2004 17:33:43 +0200 |
added Complex/root
|
file | diff | annotate |
| Mon, 12 Jul 2004 12:11:46 +0200 |
*** empty log message ***
|
file | diff | annotate |
| Thu, 01 Jul 2004 12:29:53 +0200 |
new treatment of binary numerals
|
file | diff | annotate |
| Tue, 29 Jun 2004 10:07:56 +0200 |
support for sparse matrices
|
file | diff | annotate |
| Sat, 29 May 2004 15:10:30 +0200 |
target 'generate';
|
file | diff | annotate |
| Wed, 19 May 2004 11:29:47 +0200 |
conversion of Hilbert_Choice to Isar script
|
file | diff | annotate |
| Tue, 18 May 2004 10:01:44 +0200 |
Modification / Installation of Provers/Arith/abel_cancel.ML for OrderedGroup.thy
|
file | diff | annotate |
| Tue, 11 May 2004 20:11:08 +0200 |
changes made due to new Ring_and_Field theory
|
file | diff | annotate |
| Fri, 07 May 2004 14:10:14 +0200 |
*** empty log message ***
|
file | diff | annotate |
| Fri, 23 Apr 2004 20:50:16 +0200 |
HOL-Matrix: document setup;
|
file | diff | annotate |
| Thu, 22 Apr 2004 10:45:56 +0200 |
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
|
file | diff | annotate |
| Mon, 19 Apr 2004 09:31:00 +0200 |
renamed HOL-Import-HOL to HOL4, added to images target
|
file | diff | annotate |
| Sat, 17 Apr 2004 00:46:22 +0200 |
added HOL-Matrix, added HOL/Matrix/ROOT.ML
|
file | diff | annotate |
| Fri, 16 Apr 2004 20:33:16 +0200 |
Moved ring stuff from ex into Ring_and_Field.
|
file | diff | annotate |
| Fri, 16 Apr 2004 18:09:24 +0200 |
Added theory with examples for quickcheck command.
|
file | diff | annotate |
| Fri, 16 Apr 2004 04:08:29 +0200 |
session graph;
|
file | diff | annotate |
| Thu, 15 Apr 2004 14:17:45 +0200 |
Added ex/Exceptions.thy
|
file | diff | annotate |
| Tue, 13 Apr 2004 09:42:40 +0200 |
Various changes to HOL-Algebra;
|
file | diff | annotate |
| Thu, 08 Apr 2004 12:49:23 +0200 |
new theory
|
file | diff | annotate |
| Fri, 02 Apr 2004 17:37:45 +0200 |
Added HOL proof importer.
|
file | diff | annotate |
| Fri, 02 Apr 2004 17:36:01 +0200 |
Tools/sat_solver.ML and Tools/prop_logic.ML added
|
file | diff | annotate |
| Thu, 01 Apr 2004 15:05:04 +0200 |
removal of Binary Trees examples prepratory to its going into AFP
|
file | diff | annotate |
| Wed, 31 Mar 2004 11:02:00 +0200 |
Lex now in AFP
|
file | diff | annotate |
| Mon, 29 Mar 2004 15:35:04 +0200 |
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
|
file | diff | annotate |
| Thu, 25 Mar 2004 05:37:32 +0100 |
moved MiniML and AVL to archive of formal proofs
|
file | diff | annotate |
| Fri, 19 Mar 2004 10:51:03 +0100 |
conversion of Hyperreal/Lim to new-style
|
file | diff | annotate |
| Mon, 08 Mar 2004 11:11:58 +0100 |
new theory of infinite sets
|
file | diff | annotate |
| Sat, 06 Mar 2004 19:32:21 +0100 |
Lex: removed last ML files
|
file | diff | annotate |
| Fri, 05 Mar 2004 15:18:59 +0100 |
Conversion of Poly to Isar script, and other tidying of HOL/Hyperreal
|
file | diff | annotate |
| Thu, 04 Mar 2004 15:49:42 +0100 |
Lex: ML -> thy
|
file | diff | annotate |
| Thu, 04 Mar 2004 12:06:07 +0100 |
new material from Avigad, and simplified treatment of division by 0
|
file | diff | annotate |
| Thu, 04 Mar 2004 10:06:13 +0100 |
Removed ML files from Lex
|
file | diff | annotate |
| Tue, 02 Mar 2004 11:05:55 +0100 |
converted Hyperreal/IntFloor to Isar script
|
file | diff | annotate |
| Tue, 02 Mar 2004 01:34:54 +0100 |
converted MiniML to Isar
|
file | diff | annotate |
| Mon, 01 Mar 2004 11:52:59 +0100 |
converted Hyperreal/HTranscendental to Isar script
|
file | diff | annotate |
| Mon, 01 Mar 2004 05:39:32 +0100 |
converted to Isar
|
file | diff | annotate |
| Thu, 26 Feb 2004 17:08:23 +0100 |
converted Hyperreal/Series to Isar script
|
file | diff | annotate |
| Thu, 26 Feb 2004 11:31:36 +0100 |
converted Hyperreal/NatStar to Isar script
|
file | diff | annotate |
| Wed, 25 Feb 2004 16:22:36 +0100 |
converted Hyperreal/HSeries to Isar script
|
file | diff | annotate |
| Tue, 24 Feb 2004 16:38:51 +0100 |
converted Hyperreal/Log and Hyperreal/HLog to Isar scripts
|
file | diff | annotate |
| Mon, 23 Feb 2004 17:33:38 +0100 |
converted HOL/Complex/NSInduct to Isar script
|
file | diff | annotate |
| Mon, 23 Feb 2004 16:35:46 +0100 |
converted HOL/Complex/NSCA to Isar script
|
file | diff | annotate |
| Sat, 21 Feb 2004 20:05:16 +0100 |
conversion of Complex/CStar to Isar script
|
file | diff | annotate |
| Sat, 21 Feb 2004 15:54:32 +0100 |
conversion of Complex/CSeries to Isar script
|
file | diff | annotate |
| Sat, 21 Feb 2004 11:43:39 +0100 |
conversion of Complex/CLim to Isar script
|
file | diff | annotate |
| Thu, 19 Feb 2004 15:57:34 +0100 |
Efficient, graph-based reasoner for linear and partial orders.
|
file | diff | annotate |
| Sun, 15 Feb 2004 10:46:37 +0100 |
Polymorphic treatment of binary arithmetic using axclasses
|
file | diff | annotate |
| Tue, 10 Feb 2004 12:02:11 +0100 |
generic of_nat and of_int functions, and generalization of iszero
|
file | diff | annotate |
| Tue, 03 Feb 2004 11:06:36 +0100 |
tidying of the complex numbers
|
file | diff | annotate |
| Mon, 02 Feb 2004 12:23:46 +0100 |
Conversion of HyperNat to Isar format and its declaration as a semiring
|
file | diff | annotate |
| Thu, 29 Jan 2004 16:51:17 +0100 |
simplifications in the hyperreals
|
file | diff | annotate |