Wed, 12 Dec 2001 20:37:31 +0100 |
wenzelm |
isatool expandshort;
|
file |
diff |
annotate
|
Mon, 21 May 2001 14:36:24 +0200 |
paulson |
X-symbols for set theory
|
file |
diff |
annotate
|
Mon, 07 Aug 2000 10:29:54 +0200 |
paulson |
instantiated Cancel_Numerals for "nat" in ZF
|
file |
diff |
annotate
|
Wed, 02 Aug 2000 16:06:54 +0200 |
paulson |
tidying and speeding up proofs
|
file |
diff |
annotate
|
Tue, 01 Aug 2000 15:28:21 +0200 |
paulson |
natify, a coercion to reduce the number of type constraints in arithmetic
|
file |
diff |
annotate
|
Thu, 06 Jul 2000 13:28:36 +0200 |
paulson |
removal of batch style, and tidying
|
file |
diff |
annotate
|
Fri, 30 Jun 2000 12:49:11 +0200 |
paulson |
more tidying
|
file |
diff |
annotate
|
Wed, 22 Mar 2000 12:45:41 +0100 |
paulson |
tidied using new "inst" rule
|
file |
diff |
annotate
|
Mon, 07 Feb 2000 15:14:02 +0100 |
paulson |
tidied some proofs
|
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
|
Wed, 03 Feb 1999 15:50:37 +0100 |
paulson |
tidied, with left_inverse & right_inverse as default simprules
|
file |
diff |
annotate
|
Mon, 01 Feb 1999 10:29:11 +0100 |
paulson |
a bit of tidying
|
file |
diff |
annotate
|
Fri, 29 Jan 1999 17:08:20 +0100 |
paulson |
expandshort
|
file |
diff |
annotate
|
Thu, 28 Jan 1999 10:21:45 +0100 |
paulson |
tidying
|
file |
diff |
annotate
|
Wed, 27 Jan 1999 10:31:31 +0100 |
paulson |
new typechecking solver for the simplifier
|
file |
diff |
annotate
|
Thu, 07 Jan 1999 18:30:55 +0100 |
paulson |
ZF: the natural numbers as a datatype
|
file |
diff |
annotate
|
Mon, 28 Dec 1998 16:54:01 +0100 |
paulson |
converted to use new primrec section
|
file |
diff |
annotate
|
Tue, 22 Sep 1998 13:50:57 +0200 |
paulson |
tidying
|
file |
diff |
annotate
|
Mon, 21 Sep 1998 23:17:28 +0200 |
oheimb |
improved addbefore and addSbefore
|
file |
diff |
annotate
|
Mon, 21 Sep 1998 10:46:58 +0200 |
paulson |
inserted space in #-1 to prevent confusion with an integer constant
|
file |
diff |
annotate
|
Thu, 06 Aug 1998 12:24:04 +0200 |
paulson |
even more tidying of Goal commands
|
file |
diff |
annotate
|
Wed, 15 Jul 1998 14:13:18 +0200 |
paulson |
More tidying and removal of "\!\!... from Goal commands
|
file |
diff |
annotate
|
Mon, 13 Jul 1998 16:42:27 +0200 |
paulson |
massive tidying of proofs
|
file |
diff |
annotate
|
Thu, 02 Jul 1998 17:58:12 +0200 |
paulson |
Renamed expand_if to split_if and setloop split_tac to addsplits,
|
file |
diff |
annotate
|
Mon, 22 Jun 1998 17:13:09 +0200 |
wenzelm |
isatool fixgoal;
|
file |
diff |
annotate
|
Wed, 24 Dec 1997 10:02:30 +0100 |
paulson |
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
|
file |
diff |
annotate
|
Wed, 05 Nov 1997 13:14:15 +0100 |
paulson |
Ran expandshort, especially to introduce Safe_tac
|
file |
diff |
annotate
|
Mon, 03 Nov 1997 12:24:13 +0100 |
wenzelm |
isatool fixclasimp;
|
file |
diff |
annotate
|
Fri, 10 Oct 1997 18:23:31 +0200 |
wenzelm |
fixed dots;
|
file |
diff |
annotate
|
Fri, 06 Jun 1997 12:48:21 +0200 |
paulson |
Better miniscoping for bounded quantifiers
|
file |
diff |
annotate
|
Fri, 03 Jan 1997 15:01:55 +0100 |
paulson |
Implicit simpsets and clasets for FOL and ZF
|
file |
diff |
annotate
|
Thu, 26 Sep 1996 15:49:54 +0200 |
paulson |
Ran expandshort; used stac instead of ssubst
|
file |
diff |
annotate
|
Tue, 23 Apr 1996 17:11:44 +0200 |
oheimb |
repaired critical proofs depending on the order inside non-confluent SimpSets,
|
file |
diff |
annotate
|
Thu, 28 Mar 1996 10:52:59 +0100 |
paulson |
Ran expandshort
|
file |
diff |
annotate
|
Tue, 26 Mar 1996 16:16:24 +0100 |
paulson |
Rewriting changes due to new arith_ss
|
file |
diff |
annotate
|
Tue, 30 Jan 1996 13:42:57 +0100 |
clasohm |
expanded tabs
|
file |
diff |
annotate
|
Mon, 16 Oct 1995 14:56:24 +0100 |
paulson |
The inverse limit construction -- thanks to Sten Agerholm
|
file |
diff |
annotate
|