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/ZF/simpdata.ML
changeset 41310 65631ca437c9
parent 40241 56fad09655a5
child 42455 6702c984bf5a 
--- a/src/ZF/simpdata.ML	Mon Dec 20 15:24:25 2010 +0100
+++ b/src/ZF/simpdata.ML	Mon Dec 20 16:44:33 2010 +0100
@@ -32,8 +32,8 @@
 val ZF_conn_pairs =
   [(@{const_name Ball}, [@{thm bspec}]),
    (@{const_name All}, [@{thm spec}]),
-   (@{const_name "op -->"}, [@{thm mp}]),
-   (@{const_name "op &"}, [@{thm conjunct1}, @{thm conjunct2}])];
+   (@{const_name imp}, [@{thm mp}]),
+   (@{const_name conj}, [@{thm conjunct1}, @{thm conjunct2}])];
 
 (*Analyse a:b, where b is rigid*)
 val ZF_mem_pairs =
isabelle