| Wed, 12 Nov 1997 12:34:43 +0100 |
oheimb |
restored last version
|
file |
diff |
annotate
|
| Wed, 12 Nov 1997 12:30:15 +0100 |
oheimb |
simpdata.ML: renamed split_prem_tac to split_asm_tac, added split_if_asm
|
file |
diff |
annotate
|
| Thu, 06 Nov 1997 10:29:37 +0100 |
paulson |
hyp_subst_tac checks if the equality has type variables and uses a suitable
|
file |
diff |
annotate
|
| Mon, 03 Nov 1997 12:09:20 +0100 |
wenzelm |
adapted to new implicit claset;
|
file |
diff |
annotate
|
| Sat, 01 Nov 1997 12:59:06 +0100 |
paulson |
New Blast_tac (and minor tidying...)
|
file |
diff |
annotate
|
| Fri, 10 Oct 1997 19:02:28 +0200 |
wenzelm |
fixed dots;
|
file |
diff |
annotate
|
| Wed, 06 Aug 1997 01:13:46 +0200 |
berghofe |
Moved some functions which used to be part of thy_data.ML
|
file |
diff |
annotate
|
| Mon, 21 Apr 1997 12:16:29 +0200 |
paulson |
New elimination rule for "unique existence"
|
file |
diff |
annotate
|
| Thu, 03 Apr 1997 10:30:23 +0200 |
paulson |
Declares overloading for if-and-only-if
|
file |
diff |
annotate
|
| Wed, 02 Apr 1997 11:30:03 +0200 |
paulson |
Installation of blast_tac
|
file |
diff |
annotate
|
| Thu, 12 Sep 1996 10:40:05 +0200 |
paulson |
Tidied many proofs, using AddIffs to let equivalences take
|
file |
diff |
annotate
|