changeset 14981 | e73f8140af78 |
parent 13641 | 63d1790a43ed |
child 15391 | 797ed46d724b |
--- a/src/HOL/Tools/datatype_rep_proofs.ML Sun Jun 20 09:30:12 2004 +0200 +++ b/src/HOL/Tools/datatype_rep_proofs.ML Mon Jun 21 10:25:57 2004 +0200 @@ -1,7 +1,6 @@ (* Title: HOL/Tools/datatype_rep_proofs.ML ID: $Id$ Author: Stefan Berghofer, TU Muenchen - License: GPL (GNU GENERAL PUBLIC LICENSE) Definitional introduction of datatypes Proof of characteristic theorems: