| Wed, 11 Jul 2007 12:01:10 +0200 | berghofe | Proof terms for meta-conjunctions are now normalized before | changeset | files |
| Wed, 11 Jul 2007 11:59:21 +0200 | berghofe | Added function norm_proof for normalizing the proof term | changeset | files |
| Wed, 11 Jul 2007 11:58:40 +0200 | berghofe | Added function rew_proof (for pre-normalizing proofs). | changeset | files |
| Wed, 11 Jul 2007 11:56:59 +0200 | berghofe | Function unify_consts moved from OldInductivePackage to PrimrecPackage. | changeset | files |
| Wed, 11 Jul 2007 11:54:21 +0200 | berghofe | Adapted to new inductive definition package. | changeset | files |
| Wed, 11 Jul 2007 11:54:03 +0200 | berghofe | Renamed accessible part for predicates to accp. | changeset | files |
| Wed, 11 Jul 2007 11:52:45 +0200 | berghofe | renamed inductive2 to inductive. | changeset | files |
| Wed, 11 Jul 2007 11:52:28 +0200 | berghofe | Renamed inductive2 to inductive. | changeset | files |