nipkow [Mon, 13 Mar 1995 09:41:20 +0100] rev 229
Removed unecessary type constraint because instantiations do not freeze type
vars any more.
nipkow [Wed, 08 Mar 1995 17:22:28 +0100] rev 228
Added dependencies on ../Provers/hypsubst.ML and removed those on
../Provers/ind.ML
nipkow [Wed, 08 Mar 1995 13:06:44 +0100] rev 227
Enforced partial evaluation of mk_case_split_tac
lcp [Wed, 01 Mar 1995 17:44:05 +0100] rev 226
Moved succ_leq_mono from IOA/example/Lemmas to Nat.ML as Suc_le_mono.
Moved less_leq_less from IOA/example/Lemmas to Nat.ML as less_le_trans.
lcp [Wed, 01 Mar 1995 17:37:09 +0100] rev 225
Proofs of inv1 and inv4 now use less_le_trans instead of
less_leq_less.
lcp [Wed, 01 Mar 1995 17:32:10 +0100] rev 224
Renamed plus_leD1 to add_leD1.
lcp [Wed, 01 Mar 1995 13:26:50 +0100] rev 223
Proved inj_onto_iff
lcp [Tue, 28 Feb 1995 10:52:55 +0100] rev 222
No longer calls maketest; instead, the Makefile writes the file
"test". And had to delete an extra ).
lcp [Tue, 28 Feb 1995 10:48:46 +0100] rev 221
Re-organised to perform the tests independently. Now test
is defined in terms of separate targets IMP, ex, etc. If ISABELLECOMP is set
wrongly then "exit 1" causes the Make to fail. Defines the macro "LOGIC" to
refer to the right command for running the object-logic. Uses "suffix
substitution" to shorten macro definitions.
lcp [Tue, 28 Feb 1995 02:02:34 +0100] rev 220
Installation of Integ (ported from ZF by Mattolini)