Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/eqrule_HOL_data.ML
changeset 16587 b34c8aa657a5
parent 16179 fa7e70be26b0
child 17521 0f1c48de39f5 
--- a/src/HOL/eqrule_HOL_data.ML	Tue Jun 28 15:26:45 2005 +0200
+++ b/src/HOL/eqrule_HOL_data.ML	Tue Jun 28 15:27:45 2005 +0200
@@ -33,7 +33,7 @@
 val tranformation_pairs =
   [("op -->", [mp]), ("op &", [conjunct1,conjunct2]),
    ("All", [spec]), ("True", []), ("False", []),
-   ("If", [if_bool_eq_conj RS iffD1])];
+   ("HOL.If", [if_bool_eq_conj RS iffD1])];
 
 (*
 val mk_atomize:      (string * thm list) list -> thm -> thm list
isabelle