src/HOLCF/IOA/meta_theory/TL.thy
changeset 10835 f4745d77e620
parent 5976 44290b71a85f
child 12028 52aa183c15bb
     1.1 --- a/src/HOLCF/IOA/meta_theory/TL.thy	Tue Jan 09 15:32:27 2001 +0100
     1.2 +++ b/src/HOLCF/IOA/meta_theory/TL.thy	Tue Jan 09 15:36:30 2001 +0100
     1.3 @@ -50,7 +50,7 @@
     1.4  
     1.5  (* this means that for nil and UU the effect is unpredictable *)
     1.6  Init_def
     1.7 -  "Init P s ==  (P (unlift (HD`s)))" 
     1.8 +  "Init P s ==  (P (unlift (HD$s)))" 
     1.9  
    1.10  suffix_def
    1.11    "suffix s2 s == ? s1. (Finite s1  & s = s1 @@ s2)" 
    1.12 @@ -62,7 +62,7 @@
    1.13    "([] P) s == ! s2. tsuffix s2 s --> P s2"
    1.14  
    1.15  Next_def
    1.16 -  "(Next P) s == if (TL`s=UU | TL`s=nil) then (P s) else P (TL`s)"
    1.17 +  "(Next P) s == if (TL$s=UU | TL$s=nil) then (P s) else P (TL$s)"
    1.18  
    1.19  Diamond_def
    1.20    "<> P == .~ ([] (.~ P))"