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/Domain/domain_axioms.ML
changeset 35499 6acef0aea07d
parent 35497 979706bd5c16
child 35513 89eddccbb93d 
--- a/src/HOLCF/Tools/Domain/domain_axioms.ML	Tue Mar 02 04:35:44 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_axioms.ML	Tue Mar 02 04:53:18 2010 -0800
@@ -154,7 +154,7 @@
           val take_const = %%:(dname^"_take");
           val lub = %%: @{const_name lub};
           val image = %%: @{const_name image};
-          val UNIV = %%: @{const_name UNIV};
+          val UNIV = @{term "UNIV :: nat set"};
           val lhs = lub $ (image $ take_const $ UNIV);
           val ax = mk_trp (lhs === ID);
         in
isabelle