src/HOL/eqrule_HOL_data.ML
changeset 16587 b34c8aa657a5
parent 16179 fa7e70be26b0
child 17521 0f1c48de39f5
     1.1 --- a/src/HOL/eqrule_HOL_data.ML	Tue Jun 28 15:26:45 2005 +0200
     1.2 +++ b/src/HOL/eqrule_HOL_data.ML	Tue Jun 28 15:27:45 2005 +0200
     1.3 @@ -33,7 +33,7 @@
     1.4  val tranformation_pairs =
     1.5    [("op -->", [mp]), ("op &", [conjunct1,conjunct2]),
     1.6     ("All", [spec]), ("True", []), ("False", []),
     1.7 -   ("If", [if_bool_eq_conj RS iffD1])];
     1.8 +   ("HOL.If", [if_bool_eq_conj RS iffD1])];
     1.9  
    1.10  (*
    1.11  val mk_atomize:      (string * thm list) list -> thm -> thm list