| Wed, 09 Oct 2002 11:07:13 +0200 |
paulson |
Re-organization of Constructible theories
|
file |
diff |
annotate
|
| Sat, 21 Sep 2002 21:10:34 +0200 |
paulson |
converted to Isar script
|
file |
diff |
annotate
|
| Sat, 07 Sep 2002 22:04:28 +0200 |
paulson |
conversion of ZF/Integ/{Int,Bin} to Isar scripts
|
file |
diff |
annotate
|
| Wed, 28 Aug 2002 13:08:50 +0200 |
paulson |
various new lemmas for Constructible
|
file |
diff |
annotate
|
| Sat, 24 Aug 2002 18:45:21 +0200 |
paulson |
conversion of ZF/IntDiv to Isar script
|
file |
diff |
annotate
|
| Thu, 15 Aug 2002 21:36:26 +0200 |
paulson |
Relativization and absoluteness for DPow!!
|
file |
diff |
annotate
|
| Tue, 13 Aug 2002 17:42:34 +0200 |
paulson |
In ZF/Constructible, moved many results from Satisfies_absolute, etc., to
|
file |
diff |
annotate
|
| Tue, 13 Aug 2002 11:03:11 +0200 |
paulson |
new file Constructible/Satisfies_absolute.thy
|
file |
diff |
annotate
|
| Tue, 30 Jul 2002 11:38:33 +0200 |
paulson |
removal of twos_compl.ML, which is not really needed
|
file |
diff |
annotate
|
| Sun, 28 Jul 2002 21:09:37 +0200 |
wenzelm |
tuned document;
|
file |
diff |
annotate
|
| Sun, 14 Jul 2002 19:59:55 +0200 |
paulson |
Removal of mono.thy
|
file |
diff |
annotate
|
| Sun, 14 Jul 2002 15:14:43 +0200 |
paulson |
improved presentation markup
|
file |
diff |
annotate
|
| Wed, 10 Jul 2002 16:54:07 +0200 |
paulson |
Fixed quantified variable name preservation for ball and bex (bounded quants)
|
file |
diff |
annotate
|
| Tue, 09 Jul 2002 23:03:21 +0200 |
paulson |
converted List to new-style
|
file |
diff |
annotate
|
| Tue, 09 Jul 2002 10:44:41 +0200 |
paulson |
new files
|
file |
diff |
annotate
|
| Thu, 04 Jul 2002 15:06:46 +0200 |
wenzelm |
Constructible/document/root.tex;
|
file |
diff |
annotate
|
| Tue, 02 Jul 2002 22:46:23 +0200 |
paulson |
conversion of QPair to Isar
|
file |
diff |
annotate
|
| Sat, 29 Jun 2002 21:33:06 +0200 |
paulson |
conversion of many files to Isar format
|
file |
diff |
annotate
|
| Sun, 23 Jun 2002 10:14:13 +0200 |
paulson |
conversion of Sum, pair to Isar script
|
file |
diff |
annotate
|
| Sat, 22 Jun 2002 18:28:46 +0200 |
paulson |
converted Bool, Trancl, Rel to Isar format
|
file |
diff |
annotate
|
| Wed, 19 Jun 2002 12:48:55 +0200 |
paulson |
added the Constructible target
|
file |
diff |
annotate
|
| Wed, 19 Jun 2002 10:44:28 +0200 |
paulson |
conversion of Cardinal to Isar script
|
file |
diff |
annotate
|
| Tue, 18 Jun 2002 10:52:08 +0200 |
paulson |
conversion of Fixedpt to Isar script
|
file |
diff |
annotate
|
| Sun, 16 Jun 2002 11:58:54 +0200 |
paulson |
conversion of CardinalArith to Isar script
|
file |
diff |
annotate
|
| Fri, 31 May 2002 15:06:06 +0200 |
paulson |
conversion of Finite to Isar format
|
file |
diff |
annotate
|
| Fri, 24 May 2002 15:24:29 +0200 |
paulson |
converted Update to Isar
|
file |
diff |
annotate
|
| Fri, 24 May 2002 13:15:37 +0200 |
paulson |
conversion of Perm to Isar. Strengthening of comp_fun_apply
|
file |
diff |
annotate
|
| Wed, 22 May 2002 17:26:34 +0200 |
paulson |
conversion of Nat to Isar
|
file |
diff |
annotate
|
| Tue, 21 May 2002 18:25:28 +0200 |
paulson |
conversion of OrdQuant.ML to Isar
|
file |
diff |
annotate
|
| Tue, 21 May 2002 13:06:36 +0200 |
paulson |
converted domrange to Isar and merged with equalities
|
file |
diff |
annotate
|
| Mon, 20 May 2002 11:45:57 +0200 |
paulson |
conversion of equalities and WF to Isar
|
file |
diff |
annotate
|
| Sat, 18 May 2002 22:22:23 +0200 |
paulson |
converted Epsilon to Isar
|
file |
diff |
annotate
|
| Sat, 18 May 2002 20:08:17 +0200 |
paulson |
converted Arith, Univ, func to Isar format!
|
file |
diff |
annotate
|
| Thu, 16 May 2002 09:16:22 +0200 |
paulson |
converting Ordinal.ML to Isar format
|
file |
diff |
annotate
|
| Mon, 13 May 2002 09:02:13 +0200 |
paulson |
converted Order.ML OrderType.ML OrderArith.ML to Isar format
|
file |
diff |
annotate
|
| Fri, 10 May 2002 22:51:18 +0200 |
paulson |
now-obsolete ML files
|
file |
diff |
annotate
|
| Mon, 15 Apr 2002 10:18:01 +0200 |
paulson |
converted theory ex/Limit to Isar script, but it still needs work!
|
file |
diff |
annotate
|
| Wed, 16 Jan 2002 17:52:06 +0100 |
paulson |
Isar version of AC
|
file |
diff |
annotate
|
| Tue, 08 Jan 2002 16:09:09 +0100 |
paulson |
Added some simprules proofs.
|
file |
diff |
annotate
|
| Sat, 29 Dec 2001 18:36:12 +0100 |
wenzelm |
tuned document sources;
|
file |
diff |
annotate
|
| Fri, 28 Dec 2001 10:11:14 +0100 |
paulson |
conversion to Isar/ZF
|
file |
diff |
annotate
|
| Tue, 25 Dec 2001 10:02:01 +0100 |
paulson |
conversion to Isar
|
file |
diff |
annotate
|
| Sat, 22 Dec 2001 19:42:35 +0100 |
paulson |
Resid converted to Isar/ZF
|
file |
diff |
annotate
|
| Thu, 20 Dec 2001 15:17:48 +0100 |
paulson |
converted some ZF/Induct examples to Isar
|
file |
diff |
annotate
|
| Wed, 19 Dec 2001 11:13:27 +0100 |
paulson |
separation of the AC part of Main into Main_ZFC, plus a few new lemmas
|
file |
diff |
annotate
|
| Sat, 08 Dec 2001 17:25:01 +0100 |
wenzelm |
added Main.ML;
|
file |
diff |
annotate
|
| Fri, 16 Nov 2001 22:11:19 +0100 |
wenzelm |
Ntree and Brouwer converted and moved to ZF/Induct;
|
file |
diff |
annotate
|
| Thu, 15 Nov 2001 18:20:13 +0100 |
wenzelm |
added Induct/Binary_Trees.thy, Induct/Tree_Forest (converted from
|
file |
diff |
annotate
|
| Wed, 14 Nov 2001 23:16:05 +0100 |
wenzelm |
added Induct/Binary_Trees.thy, Induct/Datatypes.thy;
|
file |
diff |
annotate
|
| Tue, 13 Nov 2001 22:20:51 +0100 |
wenzelm |
rearranged inductive package for Isar;
|
file |
diff |
annotate
|
| Wed, 07 Nov 2001 18:12:12 +0100 |
paulson |
Sidi Ehmety's port of the fold_set operator and multisets to ZF.
|
file |
diff |
annotate
|
| Wed, 07 Nov 2001 12:29:07 +0100 |
paulson |
reorganization of the ZF examples
|
file |
diff |
annotate
|
| Wed, 08 Aug 2001 14:33:10 +0200 |
paulson |
new ZF/UNITY theory
|
file |
diff |
annotate
|
| Fri, 06 Jul 2001 16:04:32 +0200 |
paulson |
two Isar tactic scripts
|
file |
diff |
annotate
|
| Tue, 26 Jun 2001 16:54:39 +0200 |
paulson |
tidying and consolidating files
|
file |
diff |
annotate
|
| Sat, 03 Feb 2001 12:41:38 +0100 |
paulson |
commutation theory, ported by Sidi Ehmety
|
file |
diff |
annotate
|
| Fri, 18 Aug 2000 12:31:20 +0200 |
paulson |
new example ZF/ex/NatSum
|
file |
diff |
annotate
|
| Fri, 11 Aug 2000 13:27:17 +0200 |
paulson |
new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers
|
file |
diff |
annotate
|
| Thu, 10 Aug 2000 11:27:34 +0200 |
paulson |
installation of cancellation simprocs for the integers
|
file |
diff |
annotate
|
| Mon, 07 Aug 2000 10:29:54 +0200 |
paulson |
instantiated Cancel_Numerals for "nat" in ZF
|
file |
diff |
annotate
|