| Fri, 11 Jan 2002 00:34:43 +0100 |
wenzelm |
moved setmksimps to Main!
|
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
|
| Wed, 14 Nov 2001 18:46:30 +0100 |
wenzelm |
adapted primrec/datatype to Isar;
|
file |
diff |
annotate
|
| Tue, 13 Nov 2001 22:20:51 +0100 |
wenzelm |
rearranged inductive package for Isar;
|
file |
diff |
annotate
|
| Fri, 09 Nov 2001 23:44:48 +0100 |
wenzelm |
tuned;
|
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, 30 Jun 2000 12:51:30 +0200 |
paulson |
removal of batch-style proofs
|
file |
diff |
annotate
|
| Wed, 28 Jun 2000 11:00:13 +0200 |
paulson |
simplified slightly by using dependencies better in theories
|
file |
diff |
annotate
|
| Fri, 05 May 2000 22:25:17 +0200 |
wenzelm |
removed Pure/section_utils.ML;
|
file |
diff |
annotate
|
| Thu, 13 Jan 2000 17:36:58 +0100 |
paulson |
new lemmas for Ntree recursor example; more simprules; more lemmas borrowed
|
file |
diff |
annotate
|
| Thu, 11 Mar 1999 13:20:35 +0100 |
wenzelm |
removed foo_build_completed -- now handled by session management (via usedir);
|
file |
diff |
annotate
|
| Mon, 08 Feb 1999 17:30:22 +0100 |
wenzelm |
~~;
|
file |
diff |
annotate
|
| Wed, 27 Jan 1999 10:31:31 +0100 |
paulson |
new typechecking solver for the simplifier
|
file |
diff |
annotate
|
| Wed, 13 Jan 1999 11:57:09 +0100 |
paulson |
datatype package improvements
|
file |
diff |
annotate
|
| Fri, 08 Jan 1999 13:20:59 +0100 |
paulson |
removal of DO_GOAL
|
file |
diff |
annotate
|
| Thu, 07 Jan 1999 18:30:55 +0100 |
paulson |
ZF: the natural numbers as a datatype
|
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
|
| Tue, 22 Sep 1998 13:50:57 +0200 |
paulson |
tidying
|
file |
diff |
annotate
|
| Fri, 18 Sep 1998 16:07:55 +0200 |
paulson |
leaves subgoal package empty
|
file |
diff |
annotate
|
| Fri, 21 Nov 1997 15:29:56 +0100 |
wenzelm |
changed Pure/Sequence interface -- isatool fixseq;
|
file |
diff |
annotate
|
| Thu, 20 Nov 1997 16:24:05 +0100 |
wenzelm |
$ISABELLE_HOME/src;
|
file |
diff |
annotate
|
| Fri, 03 Jan 1997 15:01:55 +0100 |
paulson |
Implicit simpsets and clasets for FOL and ZF
|
file |
diff |
annotate
|
| Fri, 16 Feb 1996 18:00:47 +0100 |
paulson |
Elimination of fully-functorial style.
|
file |
diff |
annotate
|
| Tue, 30 Jan 1996 13:42:57 +0100 |
clasohm |
expanded tabs
|
file |
diff |
annotate
|
| Tue, 21 Nov 1995 15:10:12 +0100 |
clasohm |
main directory is now read by exit_use_dir, too;
|
file |
diff |
annotate
|
| Tue, 24 Oct 1995 14:50:24 +0100 |
clasohm |
added calls of init_html and make_chart
|
file |
diff |
annotate
|
| Tue, 25 Apr 1995 10:56:49 +0200 |
lcp |
Now loads the theory "Let". Could add it to FOL, but this appears to
|
file |
diff |
annotate
|
| Fri, 16 Dec 1994 18:07:12 +0100 |
lcp |
changed useless "qed" calls for lemmas back to uses of "result",
|
file |
diff |
annotate
|