src/HOLCF/IOA/meta_theory/SimCorrectness.thy
changeset 10835 f4745d77e620
parent 4565 ea467ce15040
child 12218 6597093b77e7
     1.1 --- a/src/HOLCF/IOA/meta_theory/SimCorrectness.thy	Tue Jan 09 15:32:27 2001 +0100
     1.2 +++ b/src/HOLCF/IOA/meta_theory/SimCorrectness.thy	Tue Jan 09 15:36:30 2001 +0100
     1.3 @@ -23,17 +23,17 @@
     1.4  corresp_ex_sim_def
     1.5    "corresp_ex_sim A R ex == let S'= (@s'.(fst ex,s'):R & s': starts_of A)
     1.6                              in 
     1.7 -                               (S',(corresp_ex_simC A R`(snd ex)) S')"
     1.8 +                               (S',(corresp_ex_simC A R$(snd ex)) S')"
     1.9  
    1.10  
    1.11  corresp_ex_simC_def
    1.12 -  "corresp_ex_simC A R  == (fix`(LAM h ex. (%s. case ex of 
    1.13 +  "corresp_ex_simC A R  == (fix$(LAM h ex. (%s. case ex of 
    1.14        nil =>  nil
    1.15      | x##xs => (flift1 (%pr. let a = (fst pr); t = (snd pr);
    1.16                                   T' = @t'. ? ex1. (t,t'):R & move A ex1 s a t' 
    1.17                               in
    1.18                                  (@cex. move A cex s a T')
    1.19 -                                 @@ ((h`xs) T'))
    1.20 -                        `x) )))"
    1.21 +                                 @@ ((h$xs) T'))
    1.22 +                        $x) )))"
    1.23   
    1.24  end
    1.25 \ No newline at end of file