Wed, 21 Oct 1998 17:57:02 +0200 | berghofe | Changed interface of inductive. | changeset | files |
Wed, 21 Oct 1998 17:55:18 +0200 | berghofe | Changed interface of rep_datatype: Characteristic theorems | changeset | files |
Wed, 21 Oct 1998 17:53:16 +0200 | berghofe | Changed interface. | changeset | files |
Wed, 21 Oct 1998 17:52:38 +0200 | berghofe | Changed interface of add_inductive: monos and con_defs are now | changeset | files |
Wed, 21 Oct 1998 17:48:02 +0200 | berghofe | Changed syntax of inductive. | changeset | files |
Wed, 21 Oct 1998 17:46:00 +0200 | berghofe | Changed syntax of rep_datatype and inductive: Theorems | changeset | files |
Wed, 21 Oct 1998 17:40:35 +0200 | berghofe | Added theorem prod_induct (needed for rep_datatype). | changeset | files |