| Wed, 13 Nov 2002 15:26:19 +0100 | berghofe | Added inductive_realizer. | changeset | files |
| Wed, 13 Nov 2002 15:25:17 +0100 | berghofe | Added InductiveRealizer package. | changeset | files |
| Wed, 13 Nov 2002 15:24:42 +0100 | berghofe | Transitive closure is now defined inductively as well. | changeset | files |
| Sat, 09 Nov 2002 00:12:25 +0100 | kleing | Hoare.ML -> hoare.ML | changeset | files |
| Fri, 08 Nov 2002 10:34:40 +0100 | paulson | Polishing. | changeset | files |
| Fri, 08 Nov 2002 10:28:29 +0100 | paulson | generalized wf_on_unit to wf_on_any_0 | changeset | files |
| Thu, 07 Nov 2002 12:35:34 +0100 | nipkow | added raw proof blocks | changeset | files |