| Sat, 14 Jun 2008 17:26:11 +0200 |
wenzelm |
removed obsolete ML_SUFFIX;
|
file |
diff |
annotate
|
| Mon, 11 Feb 2008 15:40:21 +0100 |
krauss |
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
|
file |
diff |
annotate
|
| Thu, 31 May 2007 12:06:31 +0200 |
wenzelm |
moved Integ files to canonical place;
|
file |
diff |
annotate
|
| Thu, 26 Apr 2007 15:42:04 +0200 |
wenzelm |
removed lagacy ML files;
|
file |
diff |
annotate
|
| Wed, 19 Oct 2005 21:52:48 +0200 |
wenzelm |
removed obsolete thy_syntax.ML;
|
file |
diff |
annotate
|
| Tue, 11 Oct 2005 13:28:05 +0200 |
wenzelm |
ML_SUFFIX in targets (experimental);
|
file |
diff |
annotate
|
| Mon, 28 Mar 2005 16:19:56 +0200 |
paulson |
conversion of UNITY to Isar scripts
|
file |
diff |
annotate
|
| Sun, 19 Sep 2004 16:51:10 +0200 |
paulson |
converting UNITY/MultisetSum.ML to Isar script
|
file |
diff |
annotate
|
| Fri, 17 Sep 2004 16:08:52 +0200 |
paulson |
converted ZF/Induct/Multiset to Isar script
|
file |
diff |
annotate
|
| Thu, 29 Jul 2004 12:15:53 +0200 |
paulson |
documents for ZF-AC and ZF-Constructible
|
file |
diff |
annotate
|
| Tue, 08 Jun 2004 16:22:30 +0200 |
paulson |
Groups, Rings and supporting lemmas
|
file |
diff |
annotate
|
| Wed, 09 Jul 2003 11:39:34 +0200 |
paulson |
converting more theories to Isar scripts, and tidying
|
file |
diff |
annotate
|
| Tue, 08 Jul 2003 11:44:30 +0200 |
paulson |
Conversion of ZF/UNITY/{FP,Union} to Isar script.
|
file |
diff |
annotate
|
| Mon, 30 Jun 2003 18:15:51 +0200 |
paulson |
Removal of UNITY/UNITYMisc, moving its theorems elsewhere.
|
file |
diff |
annotate
|
| Fri, 27 Jun 2003 18:40:25 +0200 |
paulson |
Conversion of theory UNITY to Isar script
|
file |
diff |
annotate
|
| Fri, 27 Jun 2003 13:15:40 +0200 |
paulson |
Conversion of AllocBase to new-style
|
file |
diff |
annotate
|
| Thu, 26 Jun 2003 15:48:33 +0200 |
paulson |
Conversion of "Merge" to Isar format
|
file |
diff |
annotate
|
| Wed, 25 Jun 2003 13:17:26 +0200 |
paulson |
Conversion of UNITY/Distributor to Isar script. General tidy-up.
|
file |
diff |
annotate
|
| Tue, 24 Jun 2003 16:32:59 +0200 |
paulson |
Converting ZF/UNITY to Isar
|
file |
diff |
annotate
|
| Fri, 20 Jun 2003 18:13:16 +0200 |
paulson |
conversion of ClientImpl to Isar script
|
file |
diff |
annotate
|
| Fri, 20 Jun 2003 12:10:45 +0200 |
paulson |
Adding the theory UNITY/AllocImpl.thy, with supporting lemmas
|
file |
diff |
annotate
|
| Thu, 29 May 2003 17:10:00 +0200 |
paulson |
Introduction of the theories UNITY/Merge, UNITY/ClientImpl
|
file |
diff |
annotate
|
| Wed, 28 May 2003 18:13:41 +0200 |
paulson |
some new ZF/UNITY material from Sidi Ehmety
|
file |
diff |
annotate
|
| Wed, 15 Jan 2003 16:45:32 +0100 |
paulson |
more new-style theories
|
file |
diff |
annotate
|
| 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
|
| Fri, 05 May 2000 22:25:17 +0200 |
wenzelm |
removed Pure/section_utils.ML;
|
file |
diff |
annotate
|
| Wed, 03 Feb 1999 17:32:10 +0100 |
wenzelm |
usedir -r;
|
file |
diff |
annotate
|
| Wed, 06 Jan 1999 13:24:33 +0100 |
paulson |
induct_tac and exhaust_tac
|
file |
diff |
annotate
|
| Mon, 28 Dec 1998 16:59:28 +0100 |
paulson |
new inductive, datatype and primrec packages, etc.
|
file |
diff |
annotate
|
| Fri, 25 Sep 1998 13:18:07 +0200 |
paulson |
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
|
file |
diff |
annotate
|
| Wed, 23 Sep 1998 10:17:11 +0200 |
paulson |
New directory Integ for the integers
|
file |
diff |
annotate
|
| Thu, 10 Sep 1998 17:34:01 +0200 |
paulson |
new file AC/WO1_WO7.thy
|
file |
diff |
annotate
|
| Fri, 17 Jul 1998 11:23:17 +0200 |
paulson |
added Main and Update
|
file |
diff |
annotate
|
| Fri, 01 May 1998 11:22:09 +0200 |
paulson |
Let.ML and Let.thy had been omitted
|
file |
diff |
annotate
|
| Wed, 07 Jan 1998 13:53:42 +0100 |
wenzelm |
improved targets;
|
file |
diff |
annotate
|
| Fri, 19 Dec 1997 10:18:58 +0100 |
wenzelm |
log files;
|
file |
diff |
annotate
|
| Mon, 07 Jul 1997 09:09:21 +0200 |
wenzelm |
eliminated chmod -w;
|
file |
diff |
annotate
|
| Tue, 06 May 1997 15:27:35 +0200 |
wenzelm |
fixed ISABELLE_OUTPUT, ISABELLE_PATH (finally?);
|
file |
diff |
annotate
|
| Fri, 25 Apr 1997 15:24:07 +0200 |
wenzelm |
removed -c option;
|
file |
diff |
annotate
|
| Thu, 20 Mar 1997 11:39:40 +0100 |
wenzelm |
isatool usedir;
|
file |
diff |
annotate
|
| Thu, 09 Jan 1997 16:01:34 +0100 |
wenzelm |
IsaMakefile for ZF;
|
file |
diff |
annotate
|