| Tue, 10 Sep 1996 11:35:23 +0200 | paulson | Now runs all Auth proofs | changeset | files |
| Tue, 10 Sep 1996 11:07:49 +0200 | paulson | Now uses DB-ROOT.ML, which is separate from ROOT.ML | changeset | files |
| Tue, 10 Sep 1996 11:07:16 +0200 | paulson | Dedicated root file for making the Auth database | changeset | files |
| Tue, 10 Sep 1996 10:48:07 +0200 | paulson | Beefed-up auto-tactic: now repeatedly simplifies if needed | changeset | files |
| Mon, 09 Sep 1996 18:58:02 +0200 | paulson | "bad" set simplifies statements of many theorems | changeset | files |
| Mon, 09 Sep 1996 18:53:41 +0200 | nipkow | added cterm_lift_inst_rule | changeset | files |
| Mon, 09 Sep 1996 17:44:20 +0200 | paulson | Stronger proofs; work for Otway-Rees | changeset | files |