changeset 7228 | ddb67dcf026c |
parent 7205 | dab2be236bfc |
child 7257 | 745cfc8871e2 |
--- a/src/HOL/Tools/datatype_rep_proofs.ML Tue Aug 17 14:00:30 1999 +0200 +++ b/src/HOL/Tools/datatype_rep_proofs.ML Tue Aug 17 14:01:39 1999 +0200 @@ -7,7 +7,7 @@ Proof of characteristic theorems: - injectivity of constructors - - distinctness of constructors (internal version) + - distinctness of constructors - induction theorem *)