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/HOLCF/Tools/pcpodef_package.ML
changeset 25723 80c06e4d4db6
parent 25701 73fbe868b4e7
child 25926 aa0eca1ccb19 
--- a/src/HOLCF/Tools/pcpodef_package.ML	Thu Dec 20 01:07:21 2007 +0100
+++ b/src/HOLCF/Tools/pcpodef_package.ML	Thu Dec 20 03:06:20 2007 +0100
@@ -72,7 +72,7 @@
       HOLogic.mk_exists ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), A));
     fun mk_admissible A =
       mk_adm ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), A));
-    fun mk_UU_mem A = HOLogic.mk_mem (Const ("Porder.UU", oldT), A);
+    fun mk_UU_mem A = HOLogic.mk_mem (Const ("Pcpo.UU", oldT), A);
     val goal = if pcpo
       then HOLogic.mk_Trueprop (HOLogic.mk_conj (mk_UU_mem set, mk_admissible set))
       else HOLogic.mk_Trueprop (HOLogic.mk_conj (mk_nonempty set, mk_admissible set));
isabelle