Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
replaced Undef by UU;
authorwenzelm
Sat, 03 Nov 2001 01:44:45 +0100
changeset 12032 0f6417c9a187
parent 12031 1b883fa9458e
child 12033 69cb2059aadc
replaced Undef by UU;
src/HOLCF/IMP/Denotational.thy file | annotate | diff | comparison | revisions 
--- a/src/HOLCF/IMP/Denotational.thy	Sat Nov 03 01:44:26 2001 +0100
+++ b/src/HOLCF/IMP/Denotational.thy	Sat Nov 03 01:44:45 2001 +0100
@@ -10,7 +10,7 @@
 
 constdefs
    dlift :: "(('a::term) discr -> 'b::pcpo) => ('a lift -> 'b)"
-  "dlift f == (LAM x. case x of Undef => UU | Def(y) => f$(Discr y))"
+  "dlift f == (LAM x. case x of UU => UU | Def(y) => f$(Discr y))"
 
 consts D :: "com => state discr -> state lift"
isabelle