Fri, 31 May 1996 19:47:23 +0200 |
oheimb |
adapted some proofs for new simplifier
|
changeset |
files
|
Fri, 31 May 1996 19:34:40 +0200 |
oheimb |
renamed le_0 to le_0_eq, to avoid confusion with le0,
|
changeset |
files
|
Fri, 31 May 1996 19:12:00 +0200 |
oheimb |
moved mem_simps and the corresponding update of !simpset from Fun.ML to Set.ML,
|
changeset |
files
|
Thu, 30 May 1996 13:31:29 +0200 |
nipkow |
Smaller logo
|
changeset |
files
|
Thu, 30 May 1996 13:29:52 +0200 |
nipkow |
Regrouped logo
|
changeset |
files
|
Wed, 29 May 1996 13:53:39 +0200 |
nipkow |
Added logo
|
changeset |
files
|
Wed, 29 May 1996 13:47:43 +0200 |
nipkow |
An Isabelle logo
|
changeset |
files
|
Wed, 29 May 1996 13:34:17 +0200 |
nipkow |
Replaced setsolver by addsolver
|
changeset |
files
|
Wed, 29 May 1996 12:03:32 +0200 |
nipkow |
Added addsolver
|
changeset |
files
|
Tue, 28 May 1996 11:19:16 +0200 |
paulson |
Simplified proof of deduction theorem
|
changeset |
files
|
Tue, 28 May 1996 11:16:38 +0200 |
paulson |
Corrected a comment in #34
|
changeset |
files
|
Fri, 24 May 1996 12:27:04 +0200 |
berghofe |
Rules pred_0, pred_Suc etc. are now stored in theorem database.
|
changeset |
files
|
Fri, 24 May 1996 11:48:18 +0200 |
nipkow |
Modified proof of "(R^=)^* = R^*" to accommodate equalityI.
|
changeset |
files
|
Fri, 24 May 1996 11:46:40 +0200 |
nipkow |
Removed junk introduced by a cvs merge.
|
changeset |
files
|