src/HOL/Tools/datatype_package.ML
changeset 18625 2db0982523fe
parent 18518 3b1dfa53e64f
child 18643 89a7978f90e1
     1.1 --- a/src/HOL/Tools/datatype_package.ML	Mon Jan 09 13:28:34 2006 +0100
     1.2 +++ b/src/HOL/Tools/datatype_package.ML	Mon Jan 09 13:29:08 2006 +0100
     1.3 @@ -341,8 +341,10 @@
     1.4  
     1.5  end;
     1.6  
     1.7 +(*Name management for ATP linkup. The suffix here must agree with the one given
     1.8 +  for notE in Clasimp.addIff*)
     1.9  fun name_notE th =
    1.10 -    Thm.name_thm (Thm.name_of_thm th ^ "_E", th RS notE);
    1.11 +    Thm.name_thm (Thm.name_of_thm th ^ "_iff1", th RS notE);
    1.12        
    1.13  fun add_rules simps case_thms size_thms rec_thms inject distinct
    1.14                    weak_case_congs cong_att =