src/HOLCF/IOA/meta_theory/CompoScheds.thy
changeset 10835 f4745d77e620
parent 3842 b55686a7b22c
child 12028 52aa183c15bb
     1.1 --- a/src/HOLCF/IOA/meta_theory/CompoScheds.thy	Tue Jan 09 15:32:27 2001 +0100
     1.2 +++ b/src/HOLCF/IOA/meta_theory/CompoScheds.thy	Tue Jan 09 15:36:30 2001 +0100
     1.3 @@ -26,10 +26,10 @@
     1.4  mkex_def  
     1.5    "mkex A B sch exA exB == 
     1.6         ((fst exA,fst exB),
     1.7 -        (mkex2 A B`sch`(snd exA)`(snd exB)) (fst exA) (fst exB))"
     1.8 +        (mkex2 A B$sch$(snd exA)$(snd exB)) (fst exA) (fst exB))"
     1.9  
    1.10  mkex2_def
    1.11 -  "mkex2 A B == (fix`(LAM h sch exA exB. (%s t. case sch of 
    1.12 +  "mkex2 A B == (fix$(LAM h sch exA exB. (%s t. case sch of 
    1.13         nil => nil
    1.14      | x##xs => 
    1.15        (case x of 
    1.16 @@ -37,25 +37,25 @@
    1.17        | Def y => 
    1.18           (if y:act A then 
    1.19               (if y:act B then 
    1.20 -                (case HD`exA of
    1.21 +                (case HD$exA of
    1.22                     Undef => UU
    1.23 -                 | Def a => (case HD`exB of
    1.24 +                 | Def a => (case HD$exB of
    1.25                                Undef => UU
    1.26                              | Def b => 
    1.27                     (y,(snd a,snd b))>>
    1.28 -                     (h`xs`(TL`exA)`(TL`exB)) (snd a) (snd b)))
    1.29 +                     (h$xs$(TL$exA)$(TL$exB)) (snd a) (snd b)))
    1.30                else
    1.31 -                (case HD`exA of
    1.32 +                (case HD$exA of
    1.33                     Undef => UU
    1.34                   | Def a => 
    1.35 -                   (y,(snd a,t))>>(h`xs`(TL`exA)`exB) (snd a) t)
    1.36 +                   (y,(snd a,t))>>(h$xs$(TL$exA)$exB) (snd a) t)
    1.37                )
    1.38            else 
    1.39               (if y:act B then 
    1.40 -                (case HD`exB of
    1.41 +                (case HD$exB of
    1.42                     Undef => UU
    1.43                   | Def b => 
    1.44 -                   (y,(s,snd b))>>(h`xs`exA`(TL`exB)) s (snd b))
    1.45 +                   (y,(s,snd b))>>(h$xs$exA$(TL$exB)) s (snd b))
    1.46               else
    1.47                 UU
    1.48               )
    1.49 @@ -67,8 +67,8 @@
    1.50         let schA = fst SchedsA; sigA = snd SchedsA; 
    1.51             schB = fst SchedsB; sigB = snd SchedsB       
    1.52         in
    1.53 -       (    {sch. Filter (%a. a:actions sigA)`sch : schA}
    1.54 -        Int {sch. Filter (%a. a:actions sigB)`sch : schB}
    1.55 +       (    {sch. Filter (%a. a:actions sigA)$sch : schA}
    1.56 +        Int {sch. Filter (%a. a:actions sigB)$sch : schB}
    1.57          Int {sch. Forall (%x. x:(actions sigA Un actions sigB)) sch},
    1.58          asig_comp sigA sigB)"
    1.59