Wed, 07 Aug 2002 16:47:36 +0200 | berghofe | Removed (now unneeded) declaration of realizers for induction on natural numbers. | changeset | files |
Wed, 07 Aug 2002 16:46:15 +0200 | berghofe | Module for defining realizers for induction and case analysis theorems | changeset | files |
Wed, 07 Aug 2002 16:44:47 +0200 | berghofe | Added calls to add_dt_realizers. | changeset | files |