src/HOLCF/IOA/meta_theory/Abstraction.thy
changeset 10835 f4745d77e620
parent 5976 44290b71a85f
child 12218 6597093b77e7
     1.1 --- a/src/HOLCF/IOA/meta_theory/Abstraction.thy	Tue Jan 09 15:32:27 2001 +0100
     1.2 +++ b/src/HOLCF/IOA/meta_theory/Abstraction.thy	Tue Jan 09 15:36:30 2001 +0100
     1.3 @@ -43,11 +43,11 @@
     1.4        temp_weakening (snd AM) (snd CL) h"
     1.5  
     1.6  cex_abs_def
     1.7 -  "cex_abs f ex == (f (fst ex), Map (%(a,t). (a,f t))`(snd ex))"
     1.8 +  "cex_abs f ex == (f (fst ex), Map (%(a,t). (a,f t))$(snd ex))"
     1.9  
    1.10  (* equals cex_abs on Sequneces -- after ex2seq application -- *)
    1.11  cex_absSeq_def
    1.12 -  "cex_absSeq f == % s. Map (%(s,a,t). (f s,a,f t))`s"
    1.13 +  "cex_absSeq f == % s. Map (%(s,a,t). (f s,a,f t))$s"
    1.14  
    1.15  weakeningIOA_def
    1.16     "weakeningIOA A C h == ! ex. ex : executions C --> cex_abs h ex : executions A"