| Tue, 27 Jul 1999 19:02:43 +0200 | paulson | installation of simplifier and classical reasoner, better rules etc | changeset | files |
| Tue, 27 Jul 1999 19:01:46 +0200 | paulson | moved the modal prover to modal.ML; installed the prover using TheoryDataFun | changeset | files |
| Tue, 27 Jul 1999 19:00:55 +0200 | paulson | split off modal.ML from provers.ML | changeset | files |
| Tue, 27 Jul 1999 18:58:40 +0200 | paulson | fixed the comments... | changeset | files |
| Tue, 27 Jul 1999 18:52:48 +0200 | paulson | a new theory containing just an axiom needed to derive imp_cong | changeset | files |
| Tue, 27 Jul 1999 18:52:23 +0200 | paulson | renamed theory LK to LK0 | changeset | files |
| Tue, 27 Jul 1999 18:52:08 +0200 | paulson | renamed LK0.ML | changeset | files |
| Tue, 27 Jul 1999 18:50:14 +0200 | paulson | Sequents/LK/Nat: new example of simplification in LK | changeset | files |