| Mon, 07 Aug 2000 10:29:54 +0200 |
paulson |
instantiated Cancel_Numerals for "nat" in ZF
|
file |
diff |
annotate
|
| Thu, 07 Jan 1999 18:30:55 +0100 |
paulson |
ZF: the natural numbers as a datatype
|
file |
diff |
annotate
|
| Thu, 07 Jan 1999 10:56:05 +0100 |
paulson |
if-then-else syntax for ZF
|
file |
diff |
annotate
|
| Mon, 13 Jul 1998 16:43:57 +0200 |
paulson |
Huge tidy-up: removal of leading \!\!
|
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
|
| Tue, 10 Mar 1998 19:02:53 +0100 |
nipkow |
Adapted proofs because of new simplification tactics.
|
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
|
| Mon, 29 Sep 1997 11:49:33 +0200 |
paulson |
Now using qed_spec_mp
|
file |
diff |
annotate
|
| Fri, 04 Apr 1997 11:33:51 +0200 |
paulson |
Another blast_tac call
|
file |
diff |
annotate
|
| Wed, 02 Apr 1997 15:36:32 +0200 |
paulson |
Mostly converted to blast_tac
|
file |
diff |
annotate
|
| Wed, 08 Jan 1997 15:04:27 +0100 |
paulson |
Removal of sum_cs and eq_cs
|
file |
diff |
annotate
|
| Fri, 03 Jan 1997 15:01:55 +0100 |
paulson |
Implicit simpsets and clasets for FOL and ZF
|
file |
diff |
annotate
|
| Tue, 08 Oct 1996 10:18:53 +0200 |
paulson |
Removed command made redundant by the new one-point rules
|
file |
diff |
annotate
|
| Fri, 29 Mar 1996 11:38:47 +0100 |
paulson |
Simplified proof of tiling_UnI
|
file |
diff |
annotate
|
| Thu, 28 Mar 1996 10:56:10 +0100 |
paulson |
Alternative proof removes dependence upon AC
|
file |
diff |
annotate
|
| Tue, 26 Mar 1996 11:32:14 +0100 |
paulson |
New example: mutilated checkerboard
|
file |
diff |
annotate
|