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
|