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