Thu, 10 Apr 1997 18:07:27 +0200 | paulson | Updated discussion and references for inductive definitions | changeset | files |
Thu, 10 Apr 1997 14:26:01 +0200 | nipkow | Deleted stupid proof at the end not needed anywhere. | changeset | files |
Thu, 10 Apr 1997 12:21:21 +0200 | nipkow | Mod because of "Turned Addsimps into AddIffs for datatype laws." | changeset | files |