Wed, 07 Aug 2002 16:49:25 +0200 | berghofe | Removed (now unneeded) declarations of realizers for induction on lists and letters. | changeset | files |
Wed, 07 Aug 2002 16:48:20 +0200 | berghofe | Added file Tools/datatype_realizer.ML | changeset | files |
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 |