Sat, 11 Mar 1995 17:46:14 +0100 | nipkow | Added type constraints to enforce correct choice of variable names. | changeset | files |
Sat, 11 Mar 1995 11:58:21 +0100 | lcp | Put freeze into the signature TACTIC for export | changeset | files |
Fri, 10 Mar 1995 10:20:18 +0100 | lcp | Removed "localize"; instead, proofs refer to their own | changeset | files |
Thu, 09 Mar 1995 10:38:30 +0100 | lcp | Commented isof(c,t) | changeset | files |
Wed, 08 Mar 1995 17:23:07 +0100 | nipkow | Added dependencies on ../Provers/hypsubst.ML and removed those on | changeset | files |
Wed, 08 Mar 1995 14:35:26 +0100 | nipkow | Replaced read by read_cterm. | changeset | files |