# HG changeset patch
# User berghofe
# Date 934891299 -7200
# Node ID ddb67dcf026c75f0aa68ad0a5b07283083f8cc81
# Parent  a8e86b8e6fd19a4aac63e5a4f67b7ee4d1e8136c
Tuned some comments.

diff -r a8e86b8e6fd1 -r ddb67dcf026c src/HOL/Tools/datatype_abs_proofs.ML
--- a/src/HOL/Tools/datatype_abs_proofs.ML	Tue Aug 17 14:00:30 1999 +0200
+++ b/src/HOL/Tools/datatype_abs_proofs.ML	Tue Aug 17 14:01:39 1999 +0200
@@ -10,7 +10,6 @@
  - case distinction (exhaustion) theorems
  - characteristic equations for primrec combinators
  - characteristic equations for case combinators
- - distinctness of constructors (external version)
  - equations for splitting "P (case ...)" expressions
  - datatype size function
  - "nchotomy" and "case_cong" theorems for TFL
diff -r a8e86b8e6fd1 -r ddb67dcf026c src/HOL/Tools/datatype_rep_proofs.ML
--- 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
 
 *)