src/HOLCF/IOA/meta_theory/TL.thy
changeset 12028 52aa183c15bb
parent 10835 f4745d77e620
child 12114 a8e860c86252
     1.1 --- a/src/HOLCF/IOA/meta_theory/TL.thy	Sat Nov 03 01:38:39 2001 +0100
     1.2 +++ b/src/HOLCF/IOA/meta_theory/TL.thy	Sat Nov 03 01:39:17 2001 +0100
     1.3 @@ -45,7 +45,7 @@
     1.4  
     1.5  unlift_def
     1.6    "unlift x == (case x of 
     1.7 -                 Undef   => arbitrary
     1.8 +                 UU   => arbitrary
     1.9                 | Def y   => y)"
    1.10  
    1.11  (* this means that for nil and UU the effect is unpredictable *)