| Wed, 13 Nov 2002 15:32:41 +0100 | berghofe | New package for constructing realizers for introduction and elimination | changeset | files |
| Wed, 13 Nov 2002 15:31:14 +0100 | berghofe | - No longer applies norm_hhf_rule | changeset | files |
| Wed, 13 Nov 2002 15:28:41 +0100 | berghofe | prove_goal' -> Goal.simple_prove_goal_cterm | changeset | files |
| Wed, 13 Nov 2002 15:27:27 +0100 | berghofe | name_of_type now replaces non-identifiers by dummy names. | changeset | files |
| 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 |