| Sat, 16 Nov 2002 22:54:39 +0100 | kleing | beautified "match" | changeset | files |
| Fri, 15 Nov 2002 18:02:25 +0100 | nipkow | added zdvd_iff_zmod_eq_0 | changeset | files |
| Wed, 13 Nov 2002 15:36:36 +0100 | berghofe | Improved function decompose. | changeset | files |
| Wed, 13 Nov 2002 15:36:06 +0100 | berghofe | - exported functions etype_of and mk_typ | changeset | files |
| Wed, 13 Nov 2002 15:35:15 +0100 | berghofe | Fixed name clash problem in forall_elim_var. | changeset | files |
| Wed, 13 Nov 2002 15:34:35 +0100 | berghofe | Added simple_prove_goal_cterm. | changeset | files |
| Wed, 13 Nov 2002 15:34:01 +0100 | berghofe | Removed (now unneeded) declarations of realizers for bar induction. | changeset | files |
| Wed, 13 Nov 2002 15:32:41 +0100 | berghofe | New package for constructing realizers for introduction and elimination | changeset | files |