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/simpdata.ML
changeset 16587 b34c8aa657a5
parent 15570 8d8c70b41bab
child 16633 208ebc9311f2 
--- a/src/HOL/simpdata.ML	Tue Jun 28 15:26:45 2005 +0200
+++ b/src/HOL/simpdata.ML	Tue Jun 28 15:27:45 2005 +0200
@@ -240,7 +240,7 @@
 val mksimps_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