# HG changeset patch
# User berghofe
# Date 901806843 -7200
# Node ID 3224d1a9a8f1227292679fd49294fb605cba3ea8
# Parent  75c6392d12746a364bed4e8aa9be40f119120389
Deleted obsolete comments.

diff -r 75c6392d1274 -r 3224d1a9a8f1 src/HOL/Tools/datatype_rep_proofs.ML
--- a/src/HOL/Tools/datatype_rep_proofs.ML	Thu Jul 30 15:52:33 1998 +0200
+++ b/src/HOL/Tools/datatype_rep_proofs.ML	Thu Jul 30 15:54:03 1998 +0200
@@ -41,14 +41,6 @@
 
 (******************************************************************************)
 
-(*----------------------------------------------------------*)
-(* Proofs dependent on concrete representation of datatypes *)
-(*                                                          *)
-(* - injectivity of constructors                            *)
-(* - distinctness of constructors (internal version)        *)
-(* - induction theorem                                      *)
-(*----------------------------------------------------------*)
-
 fun representation_proofs (dt_info : datatype_info Symtab.table)
       new_type_names descr sorts types_syntax constr_syntax thy =
   let