src/HOLCF/IOA/meta_theory/RefCorrectness.thy
changeset 10835 f4745d77e620
parent 5976 44290b71a85f
child 12218 6597093b77e7
     1.1 --- a/src/HOLCF/IOA/meta_theory/RefCorrectness.thy	Tue Jan 09 15:32:27 2001 +0100
     1.2 +++ b/src/HOLCF/IOA/meta_theory/RefCorrectness.thy	Tue Jan 09 15:36:30 2001 +0100
     1.3 @@ -20,15 +20,15 @@
     1.4  defs
     1.5  
     1.6  corresp_ex_def
     1.7 -  "corresp_ex A f ex == (f (fst ex),(corresp_exC A f`(snd ex)) (fst ex))"
     1.8 +  "corresp_ex A f ex == (f (fst ex),(corresp_exC A f$(snd ex)) (fst ex))"
     1.9  
    1.10  
    1.11  corresp_exC_def
    1.12 -  "corresp_exC A f  == (fix`(LAM h ex. (%s. case ex of 
    1.13 +  "corresp_exC A f  == (fix$(LAM h ex. (%s. case ex of 
    1.14        nil =>  nil
    1.15      | x##xs => (flift1 (%pr. (@cex. move A cex (f s) (fst pr) (f (snd pr)))
    1.16 -                              @@ ((h`xs) (snd pr)))
    1.17 -                        `x) )))"
    1.18 +                              @@ ((h$xs) (snd pr)))
    1.19 +                        $x) )))"
    1.20   
    1.21  is_fair_ref_map_def
    1.22    "is_fair_ref_map f C A ==