Thu, 13 Jul 2000 23:13:52 +0200 |
wenzelm |
fixed comment;
|
file |
diff |
annotate
|
Thu, 29 Jun 2000 12:19:27 +0200 |
paulson |
tidied proofs using default rule equalityCE
|
file |
diff |
annotate
|
Wed, 28 Jun 2000 10:49:10 +0200 |
paulson |
tidied
|
file |
diff |
annotate
|
Wed, 21 Jun 2000 15:58:23 +0200 |
wenzelm |
fixed deps;
|
file |
diff |
annotate
|
Mon, 21 Feb 2000 11:15:43 +0100 |
paulson |
new examples that cannot be done in LEO
|
file |
diff |
annotate
|
Fri, 27 Aug 1999 15:44:27 +0200 |
paulson |
the bij predicate forced renaming of a variable bij
|
file |
diff |
annotate
|
Fri, 05 Feb 1999 17:31:42 +0100 |
paulson |
tidied Schroeder-Bernstein proof
|
file |
diff |
annotate
|
Wed, 03 Feb 1999 13:26:07 +0100 |
paulson |
inj is now a translation of inj_on
|
file |
diff |
annotate
|
Wed, 20 Jan 1999 10:33:34 +0100 |
paulson |
renamed variables for clarity
|
file |
diff |
annotate
|
Mon, 02 Nov 1998 12:35:14 +0100 |
paulson |
increased precedence of unary minus from 80 to 100
|
file |
diff |
annotate
|
Thu, 22 Oct 1998 10:58:50 +0200 |
paulson |
standard Blast_tac demos
|
file |
diff |
annotate
|
Tue, 15 Sep 1998 15:04:07 +0200 |
paulson |
From Compl(A) to -A
|
file |
diff |
annotate
|
Mon, 07 Sep 1998 10:46:48 +0200 |
paulson |
new example; tidying
|
file |
diff |
annotate
|
Mon, 27 Apr 1998 16:45:27 +0200 |
nipkow |
Renamed expand_const -> split_const.
|
file |
diff |
annotate
|
Sat, 07 Mar 1998 16:29:29 +0100 |
nipkow |
Removed `addsplits [expand_if]'
|
file |
diff |
annotate
|
Fri, 28 Nov 1997 10:52:32 +0100 |
paulson |
New example
|
file |
diff |
annotate
|
Wed, 05 Nov 1997 13:23:46 +0100 |
paulson |
Ran expandshort, especially to introduce Safe_tac
|
file |
diff |
annotate
|
Tue, 04 Nov 1997 09:26:15 +0100 |
wenzelm |
isatool fixclasimp;
|
file |
diff |
annotate
|
Mon, 03 Nov 1997 12:13:18 +0100 |
wenzelm |
isatool fixclasimp;
|
file |
diff |
annotate
|
Fri, 17 Oct 1997 15:25:12 +0200 |
nipkow |
setloop split_tac -> addsplits
|
file |
diff |
annotate
|
Fri, 10 Oct 1997 19:02:28 +0200 |
wenzelm |
fixed dots;
|
file |
diff |
annotate
|
Mon, 21 Apr 1997 10:15:00 +0200 |
paulson |
New blast_tac demo
|
file |
diff |
annotate
|
Fri, 11 Apr 1997 15:21:36 +0200 |
paulson |
Yet more fast_tac->blast_tac, and other tidying
|
file |
diff |
annotate
|
Fri, 04 Apr 1997 16:27:39 +0200 |
nipkow |
Inv -> inv
|
file |
diff |
annotate
|
Thu, 26 Sep 1996 12:47:47 +0200 |
paulson |
Ran expandshort
|
file |
diff |
annotate
|
Fri, 26 Jul 1996 12:25:15 +0200 |
paulson |
Removal of cfast_tac
|
file |
diff |
annotate
|
Fri, 21 Jun 1996 12:18:50 +0200 |
berghofe |
Classical tactics now use default claset.
|
file |
diff |
annotate
|
Fri, 09 Feb 1996 13:43:07 +0100 |
nipkow |
replace sstac
|
file |
diff |
annotate
|
Tue, 30 Jan 1996 15:24:36 +0100 |
clasohm |
expanded tabs
|
file |
diff |
annotate
|
Wed, 22 Mar 1995 12:42:34 +0100 |
clasohm |
converted ex with curried function application
|
file |
diff |
annotate
|