# HG changeset patch
# User nipkow
# Date 979050990 -3600
# Node ID f4745d77e620ce749abbb573b147de11ee0e0258
# Parent  a7897aebbffc6ba75e5f9a688b7b6bdb0fa4da8e
` -> $

diff -r a7897aebbffc -r f4745d77e620 src/HOLCF/IMP/Denotational.ML
--- a/src/HOLCF/IMP/Denotational.ML	Tue Jan 09 15:32:27 2001 +0100
+++ b/src/HOLCF/IMP/Denotational.ML	Tue Jan 09 15:36:30 2001 +0100
@@ -6,7 +6,7 @@
 Equivalence of Denotational Semantics in HOLCF and Evaluation Semantics in HOL
 *)
 
-Goalw [dlift_def] "dlift f`(Def x) = f`(Discr x)";
+Goalw [dlift_def] "dlift f$(Def x) = f$(Discr x)";
 by (Simp_tac 1);
 qed "dlift_Def";
 Addsimps [dlift_Def];
@@ -17,18 +17,18 @@
 AddIffs [cont_dlift];
 
 Goalw [dlift_def]
- "(dlift f`l = Def y) = (? x. l = Def x & f`(Discr x) = Def y)";
+ "(dlift f$l = Def y) = (? x. l = Def x & f$(Discr x) = Def y)";
 by (simp_tac (simpset() addsplits [Lift1.lift.split]) 1);
 qed "dlift_is_Def";
 Addsimps [dlift_is_Def];
 
-Goal "<c,s> -c-> t ==> D c`(Discr s) = (Def t)";
+Goal "<c,s> -c-> t ==> D c$(Discr s) = (Def t)";
 by (etac evalc.induct 1);
       by (ALLGOALS Asm_simp_tac);
  by (ALLGOALS (stac fix_eq THEN' Asm_full_simp_tac));
 qed_spec_mp "eval_implies_D";
 
-Goal "!s t. D c`(Discr s) = (Def t) --> <c,s> -c-> t";
+Goal "!s t. D c$(Discr s) = (Def t) --> <c,s> -c-> t";
 by (induct_tac "c" 1);
     by (Force_tac 1);
    by (Force_tac 1);
@@ -46,6 +46,6 @@
 qed_spec_mp "D_implies_eval";
 
 
-Goal "(D c`(Discr s) = (Def t)) = (<c,s> -c-> t)";
+Goal "(D c$(Discr s) = (Def t)) = (<c,s> -c-> t)";
 by (fast_tac (claset() addSEs [D_implies_eval,eval_implies_D]) 1);
 qed "D_is_eval";
diff -r a7897aebbffc -r f4745d77e620 src/HOLCF/IMP/Denotational.thy
--- a/src/HOLCF/IMP/Denotational.thy	Tue Jan 09 15:32:27 2001 +0100
+++ b/src/HOLCF/IMP/Denotational.thy	Tue Jan 09 15:36:30 2001 +0100
@@ -10,7 +10,7 @@
 
 constdefs
    dlift :: "(('a::term) discr -> 'b::pcpo) => ('a lift -> 'b)"
-  "dlift f == (LAM x. case x of Undef => UU | Def(y) => f`(Discr y))"
+  "dlift f == (LAM x. case x of Undef => UU | Def(y) => f$(Discr y))"
 
 consts D :: "com => state discr -> state lift"
 
@@ -19,9 +19,9 @@
   "D(X :== a) = (LAM s. Def((undiscr s)[X ::= a(undiscr s)]))"
   "D(c0 ; c1) = (dlift(D c1) oo (D c0))"
   "D(IF b THEN c1 ELSE c2) =
-	(LAM s. if b(undiscr s) then (D c1)`s else (D c2)`s)"
+	(LAM s. if b(undiscr s) then (D c1)$s else (D c2)$s)"
   "D(WHILE b DO c) =
-	fix`(LAM w s. if b(undiscr s) then (dlift w)`((D c)`s)
+	fix$(LAM w s. if b(undiscr s) then (dlift w)$((D c)$s)
                       else Def(undiscr s))"
 
 end
diff -r a7897aebbffc -r f4745d77e620 src/HOLCF/IMP/HoareEx.thy
--- a/src/HOLCF/IMP/HoareEx.thy	Tue Jan 09 15:32:27 2001 +0100
+++ b/src/HOLCF/IMP/HoareEx.thy	Tue Jan 09 15:36:30 2001 +0100
@@ -13,6 +13,6 @@
 types assn = state => bool
 
 constdefs hoare_valid :: [assn,com,assn] => bool ("|= {(1_)}/ (_)/ {(1_)}" 50)
- "|= {A} c {B} == !s t. A s & D c `(Discr s) = Def t --> B t"
+ "|= {A} c {B} == !s t. A s & D c $(Discr s) = Def t --> B t"
 
 end
diff -r a7897aebbffc -r f4745d77e620 src/HOLCF/IOA/meta_theory/Abstraction.ML
--- a/src/HOLCF/IOA/meta_theory/Abstraction.ML	Tue Jan 09 15:32:27 2001 +0100
+++ b/src/HOLCF/IOA/meta_theory/Abstraction.ML	Tue Jan 09 15:36:30 2001 +0100
@@ -181,7 +181,7 @@
    that is to special Map Lemma *)
 Goalw [cex_abs_def,mk_trace_def,filter_act_def]
   "ext C = ext A \
-\        ==> mk_trace C`xs = mk_trace A`(snd (cex_abs f (s,xs)))";
+\        ==> mk_trace C$xs = mk_trace A$(snd (cex_abs f (s,xs)))";
 by (Asm_full_simp_tac 1);
 by (pair_induct_tac "xs" [] 1);
 qed"traces_coincide_abs";
@@ -383,11 +383,11 @@
 
 (* FIX: NAch Sequence.ML bringen *)
 
-Goal "(Map f`s = nil) = (s=nil)";
+Goal "(Map f$s = nil) = (s=nil)";
 by (Seq_case_simp_tac "s" 1);
 qed"Mapnil";
 
-Goal "(Map f`s = UU) = (s=UU)";
+Goal "(Map f$s = UU) = (s=UU)";
 by (Seq_case_simp_tac "s" 1);
 qed"MapUU";
 
@@ -400,7 +400,7 @@
 by Auto_tac;
 by (asm_full_simp_tac (simpset() addsimps [Mapnil])1);
 by (asm_full_simp_tac (simpset() addsimps [MapUU])1);
-by (res_inst_tac [("x","Map (%(s,a,t). (h s,a, h t))`s1")] exI 1);
+by (res_inst_tac [("x","Map (%(s,a,t). (h s,a, h t))$s1")] exI 1);
 by (asm_full_simp_tac (simpset() addsimps [Map2Finite,MapConc])1);
 qed"cex_absSeq_tsuffix";
 
@@ -433,7 +433,7 @@
 (* ------------------ Next ----------------------------*)
 
 Goal 
-"(TL`(ex2seq (cex_abs h ex))=UU) = (TL`(ex2seq ex)=UU)";
+"(TL$(ex2seq (cex_abs h ex))=UU) = (TL$(ex2seq ex)=UU)";
 by (pair_tac "ex" 1);
 by (Seq_case_simp_tac "y" 1);
 by (pair_tac "a" 1);
@@ -442,7 +442,7 @@
 qed"TL_ex2seq_UU";
 
 Goal 
-"(TL`(ex2seq (cex_abs h ex))=nil) = (TL`(ex2seq ex)=nil)";
+"(TL$(ex2seq (cex_abs h ex))=nil) = (TL$(ex2seq ex)=nil)";
 by (pair_tac "ex" 1);
 by (Seq_case_simp_tac "y" 1);
 by (pair_tac "a" 1);
@@ -451,7 +451,7 @@
 qed"TL_ex2seq_nil";
 
 (* FIX: put to Sequence Lemmas *)
-Goal "Map f`(TL`s) = TL`(Map f`s)";
+Goal "Map f$(TL$s) = TL$(Map f$s)";
 by (Seq_induct_tac "s" [] 1);
 qed"MapTL";
 
@@ -459,13 +459,13 @@
   properties carry over *)
 
 Goalw [cex_absSeq_def]
-"cex_absSeq h (TL`s) = (TL`(cex_absSeq h s))";
+"cex_absSeq h (TL$s) = (TL$(cex_absSeq h s))";
 by (simp_tac (simpset() addsimps [MapTL]) 1);
 qed"cex_absSeq_TL";
 
 (* important property of ex2seq: can be shiftet, as defined "pointwise" *)
 
-Goal "[| (snd ex)~=UU ; (snd ex)~=nil |] ==> (? ex'. TL`(ex2seq ex) = ex2seq ex')";
+Goal "[| (snd ex)~=UU ; (snd ex)~=nil |] ==> (? ex'. TL$(ex2seq ex) = ex2seq ex')";
 by (pair_tac "ex" 1);
 by (Seq_case_simp_tac "y" 1);
 by (pair_tac "a" 1);
@@ -473,7 +473,7 @@
 qed"TLex2seq";
 
  
-Goal "(TL`(ex2seq ex)~=nil) = ((snd ex)~=nil & (snd ex)~=UU)";
+Goal "(TL$(ex2seq ex)~=nil) = ((snd ex)~=nil & (snd ex)~=UU)";
 by (pair_tac "ex" 1);
 by (Seq_case_simp_tac "y" 1);
 by (pair_tac "a" 1);
diff -r a7897aebbffc -r f4745d77e620 src/HOLCF/IOA/meta_theory/Abstraction.thy
--- a/src/HOLCF/IOA/meta_theory/Abstraction.thy	Tue Jan 09 15:32:27 2001 +0100
+++ b/src/HOLCF/IOA/meta_theory/Abstraction.thy	Tue Jan 09 15:36:30 2001 +0100
@@ -43,11 +43,11 @@
       temp_weakening (snd AM) (snd CL) h"
 
 cex_abs_def
-  "cex_abs f ex == (f (fst ex), Map (%(a,t). (a,f t))`(snd ex))"
+  "cex_abs f ex == (f (fst ex), Map (%(a,t). (a,f t))$(snd ex))"
 
 (* equals cex_abs on Sequneces -- after ex2seq application -- *)
 cex_absSeq_def
-  "cex_absSeq f == % s. Map (%(s,a,t). (f s,a,f t))`s"
+  "cex_absSeq f == % s. Map (%(s,a,t). (f s,a,f t))$s"
 
 weakeningIOA_def
    "weakeningIOA A C h == ! ex. ex : executions C --> cex_abs h ex : executions A"
diff -r a7897aebbffc -r f4745d77e620 src/HOLCF/IOA/meta_theory/CompoExecs.ML
--- a/src/HOLCF/IOA/meta_theory/CompoExecs.ML	Tue Jan 09 15:32:27 2001 +0100
+++ b/src/HOLCF/IOA/meta_theory/CompoExecs.ML	Tue Jan 09 15:36:30 2001 +0100
@@ -20,15 +20,15 @@
 (* ---------------------------------------------------------------- *)
 
 
-Goal  "ProjA2`UU = UU";
+Goal  "ProjA2$UU = UU";
 by (simp_tac (simpset() addsimps [ProjA2_def]) 1);
 qed"ProjA2_UU";
 
-Goal  "ProjA2`nil = nil";
+Goal  "ProjA2$nil = nil";
 by (simp_tac (simpset() addsimps [ProjA2_def]) 1);
 qed"ProjA2_nil";
 
-Goal "ProjA2`((a,t)>>xs) = (a,fst t) >> ProjA2`xs";
+Goal "ProjA2$((a,t)>>xs) = (a,fst t) >> ProjA2$xs";
 by (simp_tac (simpset() addsimps [ProjA2_def]) 1);
 qed"ProjA2_cons";
 
@@ -38,15 +38,15 @@
 (* ---------------------------------------------------------------- *)
 
 
-Goal  "ProjB2`UU = UU";
+Goal  "ProjB2$UU = UU";
 by (simp_tac (simpset() addsimps [ProjB2_def]) 1);
 qed"ProjB2_UU";
 
-Goal  "ProjB2`nil = nil";
+Goal  "ProjB2$nil = nil";
 by (simp_tac (simpset() addsimps [ProjB2_def]) 1);
 qed"ProjB2_nil";
 
-Goal "ProjB2`((a,t)>>xs) = (a,snd t) >> ProjB2`xs";
+Goal "ProjB2$((a,t)>>xs) = (a,snd t) >> ProjB2$xs";
 by (simp_tac (simpset() addsimps [ProjB2_def]) 1);
 qed"ProjB2_cons";
 
@@ -57,18 +57,18 @@
 (* ---------------------------------------------------------------- *)
 
 
-Goal "Filter_ex2 sig`UU=UU";
+Goal "Filter_ex2 sig$UU=UU";
 by (simp_tac (simpset() addsimps [Filter_ex2_def]) 1);
 qed"Filter_ex2_UU";
 
-Goal "Filter_ex2 sig`nil=nil";
+Goal "Filter_ex2 sig$nil=nil";
 by (simp_tac (simpset() addsimps [Filter_ex2_def]) 1);
 qed"Filter_ex2_nil";
 
-Goal "Filter_ex2 sig`(at >> xs) =    \
+Goal "Filter_ex2 sig$(at >> xs) =    \
 \            (if (fst at:actions sig)    \       
-\                 then at >> (Filter_ex2 sig`xs) \   
-\                 else        Filter_ex2 sig`xs)";
+\                 then at >> (Filter_ex2 sig$xs) \   
+\                 else        Filter_ex2 sig$xs)";
 
 by (asm_full_simp_tac (simpset() addsimps [Filter_ex2_def]) 1);
 qed"Filter_ex2_cons";
@@ -85,8 +85,8 @@
 \            (%p.(If Def ((fst p)~:actions sig) \
 \                 then Def (s=(snd p)) \
 \                 else TT fi) \
-\                andalso (stutter2 sig`xs) (snd p))  \
-\             `x) \
+\                andalso (stutter2 sig$xs) (snd p))  \
+\             $x) \
 \           ))";
 by (rtac trans 1);
 by (rtac fix_eq2 1);
@@ -95,19 +95,19 @@
 by (simp_tac (simpset() addsimps [flift1_def]) 1);
 qed"stutter2_unfold";
 
-Goal "(stutter2 sig`UU) s=UU";
+Goal "(stutter2 sig$UU) s=UU";
 by (stac stutter2_unfold 1);
 by (Simp_tac 1);
 qed"stutter2_UU";
 
-Goal "(stutter2 sig`nil) s = TT";
+Goal "(stutter2 sig$nil) s = TT";
 by (stac stutter2_unfold 1);
 by (Simp_tac 1);
 qed"stutter2_nil";
 
-Goal "(stutter2 sig`(at>>xs)) s = \
+Goal "(stutter2 sig$(at>>xs)) s = \
 \              ((if (fst at)~:actions sig then Def (s=snd at) else TT) \
-\                andalso (stutter2 sig`xs) (snd at))"; 
+\                andalso (stutter2 sig$xs) (snd at))"; 
 by (rtac trans 1);
 by (stac stutter2_unfold 1);
 by (asm_full_simp_tac (simpset() addsimps [Consq_def,flift1_def,If_and_if]) 1);
@@ -159,8 +159,8 @@
 (* --------------------------------------------------------------------- *)
 
 Goal "!s. is_exec_frag (A||B) (s,xs) \
-\      -->  is_exec_frag A (fst s, Filter_ex2 (asig_of A)`(ProjA2`xs)) &\
-\           is_exec_frag B (snd s, Filter_ex2 (asig_of B)`(ProjB2`xs))";
+\      -->  is_exec_frag A (fst s, Filter_ex2 (asig_of A)$(ProjA2$xs)) &\
+\           is_exec_frag B (snd s, Filter_ex2 (asig_of B)$(ProjB2$xs))";
 
 by (pair_induct_tac "xs" [is_exec_frag_def] 1);
 (* main case *)
@@ -175,8 +175,8 @@
 (* --------------------------------------------------------------------- *)
 
 Goal "!s. is_exec_frag (A||B) (s,xs) \
-\      --> stutter (asig_of A) (fst s,ProjA2`xs)  &\
-\          stutter (asig_of B) (snd s,ProjB2`xs)"; 
+\      --> stutter (asig_of A) (fst s,ProjA2$xs)  &\
+\          stutter (asig_of B) (snd s,ProjB2$xs)"; 
 
 by (pair_induct_tac "xs" [stutter_def,is_exec_frag_def] 1);
 (* main case *)
@@ -205,10 +205,10 @@
 (* ----------------------------------------------------------------------- *)
 
 Goal 
-"!s. is_exec_frag A (fst s,Filter_ex2 (asig_of A)`(ProjA2`xs)) &\
-\    is_exec_frag B (snd s,Filter_ex2 (asig_of B)`(ProjB2`xs)) &\
-\    stutter (asig_of A) (fst s,(ProjA2`xs)) & \
-\    stutter (asig_of B) (snd s,(ProjB2`xs)) & \
+"!s. is_exec_frag A (fst s,Filter_ex2 (asig_of A)$(ProjA2$xs)) &\
+\    is_exec_frag B (snd s,Filter_ex2 (asig_of B)$(ProjB2$xs)) &\
+\    stutter (asig_of A) (fst s,(ProjA2$xs)) & \
+\    stutter (asig_of B) (snd s,(ProjB2$xs)) & \
 \    Forall (%x. fst x:act (A||B)) xs \
 \    --> is_exec_frag (A||B) (s,xs)";
 
diff -r a7897aebbffc -r f4745d77e620 src/HOLCF/IOA/meta_theory/CompoExecs.thy
--- a/src/HOLCF/IOA/meta_theory/CompoExecs.thy	Tue Jan 09 15:32:27 2001 +0100
+++ b/src/HOLCF/IOA/meta_theory/CompoExecs.thy	Tue Jan 09 15:36:30 2001 +0100
@@ -27,10 +27,10 @@
 
 
 ProjA_def
- "ProjA ex == (fst (fst ex), ProjA2`(snd ex))" 
+ "ProjA ex == (fst (fst ex), ProjA2$(snd ex))" 
 
 ProjB_def
- "ProjB ex == (snd (fst ex), ProjB2`(snd ex))" 
+ "ProjB ex == (snd (fst ex), ProjB2$(snd ex))" 
 
 
 ProjA2_def
@@ -41,24 +41,24 @@
  
 
 Filter_ex_def
-  "Filter_ex sig ex == (fst ex,Filter_ex2 sig`(snd ex))"
+  "Filter_ex sig ex == (fst ex,Filter_ex2 sig$(snd ex))"
 
 
 Filter_ex2_def
   "Filter_ex2 sig ==  Filter (%x. fst x:actions sig)"
 
 stutter_def
-  "stutter sig ex == ((stutter2 sig`(snd ex)) (fst ex) ~= FF)"
+  "stutter sig ex == ((stutter2 sig$(snd ex)) (fst ex) ~= FF)"
 
 stutter2_def
-  "stutter2 sig ==(fix`(LAM h ex. (%s. case ex of 
+  "stutter2 sig ==(fix$(LAM h ex. (%s. case ex of 
       nil => TT
     | x##xs => (flift1 
             (%p.(If Def ((fst p)~:actions sig)
                  then Def (s=(snd p)) 
                  else TT fi)
-                andalso (h`xs) (snd p)) 
-             `x)
+                andalso (h$xs) (snd p)) 
+             $x)
    )))" 
 
 par_execs_def
diff -r a7897aebbffc -r f4745d77e620 src/HOLCF/IOA/meta_theory/CompoScheds.ML
--- a/src/HOLCF/IOA/meta_theory/CompoScheds.ML	Tue Jan 09 15:32:27 2001 +0100
+++ b/src/HOLCF/IOA/meta_theory/CompoScheds.ML	Tue Jan 09 15:36:30 2001 +0100
@@ -30,25 +30,25 @@
 \     | Def y =>  \
 \        (if y:act A then \
 \            (if y:act B then \
-\               (case HD`exA of \
+\               (case HD$exA of \
 \                  Undef => UU \
-\                | Def a => (case HD`exB of \
+\                | Def a => (case HD$exB of \
 \                             Undef => UU \
 \                           | Def b => \
 \                  (y,(snd a,snd b))>>  \
-\                    (mkex2 A B`xs`(TL`exA)`(TL`exB)) (snd a) (snd b)))  \
+\                    (mkex2 A B$xs$(TL$exA)$(TL$exB)) (snd a) (snd b)))  \
 \             else   \
-\               (case HD`exA of   \
+\               (case HD$exA of   \
 \                  Undef => UU  \
 \                | Def a => \
-\                  (y,(snd a,t))>>(mkex2 A B`xs`(TL`exA)`exB) (snd a) t)  \
+\                  (y,(snd a,t))>>(mkex2 A B$xs$(TL$exA)$exB) (snd a) t)  \
 \             )  \       
 \         else   \
 \            (if y:act B then \
-\               (case HD`exB of  \
+\               (case HD$exB of  \
 \                  Undef => UU  \
 \                | Def b =>  \
-\                  (y,(s,snd b))>>(mkex2 A B`xs`exA`(TL`exB)) s (snd b))  \
+\                  (y,(s,snd b))>>(mkex2 A B$xs$exA$(TL$exB)) s (snd b))  \
 \            else  \
 \              UU  \
 \            )  \
@@ -56,38 +56,38 @@
 \      )))");
 
 
-Goal "(mkex2 A B`UU`exA`exB) s t = UU";
+Goal "(mkex2 A B$UU$exA$exB) s t = UU";
 by (stac mkex2_unfold 1);
 by (Simp_tac 1);
 qed"mkex2_UU";
 
-Goal "(mkex2 A B`nil`exA`exB) s t= nil";
+Goal "(mkex2 A B$nil$exA$exB) s t= nil";
 by (stac mkex2_unfold 1);
 by (Simp_tac 1);
 qed"mkex2_nil";
 
-Goal "[| x:act A; x~:act B; HD`exA=Def a|] \
-\   ==> (mkex2 A B`(x>>sch)`exA`exB) s t =   \
-\       (x,snd a,t) >> (mkex2 A B`sch`(TL`exA)`exB) (snd a) t";
+Goal "[| x:act A; x~:act B; HD$exA=Def a|] \
+\   ==> (mkex2 A B$(x>>sch)$exA$exB) s t =   \
+\       (x,snd a,t) >> (mkex2 A B$sch$(TL$exA)$exB) (snd a) t";
 by (rtac trans 1);
 by (stac mkex2_unfold 1);
 by (asm_full_simp_tac (simpset() addsimps [Consq_def,If_and_if]) 1);
 by (asm_full_simp_tac (simpset() addsimps [Consq_def]) 1);
 qed"mkex2_cons_1";
 
-Goal "[| x~:act A; x:act B; HD`exB=Def b|] \
-\   ==> (mkex2 A B`(x>>sch)`exA`exB) s t = \
-\       (x,s,snd b) >> (mkex2 A B`sch`exA`(TL`exB)) s (snd b)";
+Goal "[| x~:act A; x:act B; HD$exB=Def b|] \
+\   ==> (mkex2 A B$(x>>sch)$exA$exB) s t = \
+\       (x,s,snd b) >> (mkex2 A B$sch$exA$(TL$exB)) s (snd b)";
 by (rtac trans 1);
 by (stac mkex2_unfold 1);
 by (asm_full_simp_tac (simpset() addsimps [Consq_def,If_and_if]) 1);
 by (asm_full_simp_tac (simpset() addsimps [Consq_def]) 1);
 qed"mkex2_cons_2";
 
-Goal "[| x:act A; x:act B; HD`exA=Def a;HD`exB=Def b|] \
-\   ==> (mkex2 A B`(x>>sch)`exA`exB) s t =  \
+Goal "[| x:act A; x:act B; HD$exA=Def a;HD$exB=Def b|] \
+\   ==> (mkex2 A B$(x>>sch)$exA$exB) s t =  \
 \        (x,snd a,snd b) >> \
-\           (mkex2 A B`sch`(TL`exA)`(TL`exB)) (snd a) (snd b)";
+\           (mkex2 A B$sch$(TL$exA)$(TL$exB)) (snd a) (snd b)";
 by (rtac trans 1);
 by (stac mkex2_unfold 1);
 by (asm_full_simp_tac (simpset() addsimps [Consq_def,If_and_if]) 1);
@@ -156,8 +156,8 @@
 (* --------------------------------------------------------------------- *)
 
 Goalw [filter_act_def,Filter_ex2_def]
-   "filter_act`(Filter_ex2 (asig_of A)`xs)=\
-\   Filter (%a. a:act A)`(filter_act`xs)";
+   "filter_act$(Filter_ex2 (asig_of A)$xs)=\
+\   Filter (%a. a:act A)$(filter_act$xs)";
 
 by (simp_tac (simpset() addsimps [MapFilter,o_def]) 1);
 qed"lemma_2_1a";
@@ -168,8 +168,8 @@
 (* --------------------------------------------------------------------- *)
 
 Goal 
-   "filter_act`(ProjA2`xs) =filter_act`xs &\
-\   filter_act`(ProjB2`xs) =filter_act`xs";
+   "filter_act$(ProjA2$xs) =filter_act$xs &\
+\   filter_act$(ProjB2$xs) =filter_act$xs";
 
 by (pair_induct_tac "xs" [] 1);
 qed"lemma_2_1b";
@@ -184,7 +184,7 @@
    is the same proposition, but we cannot change this one, when then rather lemma_1_1c  *)
 
 Goal "!s. is_exec_frag (A||B) (s,xs) \
-\  --> Forall (%x. x:act (A||B)) (filter_act`xs)";
+\  --> Forall (%x. x:act (A||B)) (filter_act$xs)";
 
 by (pair_induct_tac "xs" [is_exec_frag_def,Forall_def,sforall_def] 1);
 (* main case *)
@@ -205,9 +205,9 @@
 
 Goal "! exA exB s t. \
 \ Forall (%x. x:act (A||B)) sch  & \
-\ Filter (%a. a:act A)`sch << filter_act`exA &\
-\ Filter (%a. a:act B)`sch << filter_act`exB \
-\ --> filter_act`(snd (mkex A B sch (s,exA) (t,exB))) = sch";
+\ Filter (%a. a:act A)$sch << filter_act$exA &\
+\ Filter (%a. a:act B)$sch << filter_act$exB \
+\ --> filter_act$(snd (mkex A B sch (s,exA) (t,exB))) = sch";
 
 by (Seq_induct_tac "sch" [Filter_def,Forall_def,sforall_def,mkex_def] 1);
 
@@ -268,9 +268,9 @@
 
 Goal "! exA exB s t. \
 \ Forall (%x. x:act (A||B)) sch & \
-\ Filter (%a. a:act A)`sch << filter_act`exA &\
-\ Filter (%a. a:act B)`sch << filter_act`exB \
-\ --> stutter (asig_of A) (s,ProjA2`(snd (mkex A B sch (s,exA) (t,exB))))";
+\ Filter (%a. a:act A)$sch << filter_act$exA &\
+\ Filter (%a. a:act B)$sch << filter_act$exB \
+\ --> stutter (asig_of A) (s,ProjA2$(snd (mkex A B sch (s,exA) (t,exB))))";
 
 by (mkex_induct_tac "sch" "exA" "exB");
 
@@ -279,8 +279,8 @@
 
 Goal "[|  \
 \ Forall (%x. x:act (A||B)) sch ; \
-\ Filter (%a. a:act A)`sch << filter_act`(snd exA) ;\
-\ Filter (%a. a:act B)`sch << filter_act`(snd exB) |] \
+\ Filter (%a. a:act A)$sch << filter_act$(snd exA) ;\
+\ Filter (%a. a:act B)$sch << filter_act$(snd exB) |] \
 \ ==> stutter (asig_of A) (ProjA (mkex A B sch exA exB))";
 
 by (cut_facts_tac [stutterA_mkex] 1);
@@ -299,9 +299,9 @@
 
 Goal "! exA exB s t. \
 \ Forall (%x. x:act (A||B)) sch & \
-\ Filter (%a. a:act A)`sch << filter_act`exA &\
-\ Filter (%a. a:act B)`sch << filter_act`exB \
-\ --> stutter (asig_of B) (t,ProjB2`(snd (mkex A B sch (s,exA) (t,exB))))";
+\ Filter (%a. a:act A)$sch << filter_act$exA &\
+\ Filter (%a. a:act B)$sch << filter_act$exB \
+\ --> stutter (asig_of B) (t,ProjB2$(snd (mkex A B sch (s,exA) (t,exB))))";
 
 by (mkex_induct_tac "sch" "exA" "exB");
 
@@ -310,8 +310,8 @@
 
 Goal "[|  \
 \ Forall (%x. x:act (A||B)) sch ; \
-\ Filter (%a. a:act A)`sch << filter_act`(snd exA) ;\
-\ Filter (%a. a:act B)`sch << filter_act`(snd exB) |] \
+\ Filter (%a. a:act A)$sch << filter_act$(snd exA) ;\
+\ Filter (%a. a:act B)$sch << filter_act$(snd exB) |] \
 \ ==> stutter (asig_of B) (ProjB (mkex A B sch exA exB))";
 
 by (cut_facts_tac [stutterB_mkex] 1);
@@ -325,40 +325,40 @@
 
 (*---------------------------------------------------------------------------
      Filter of mkex(sch,exA,exB) to A after projection onto A is exA 
-        --  using zip`(proj1`exA)`(proj2`exA) instead of exA    --
+        --  using zip$(proj1$exA)$(proj2$exA) instead of exA    --
         --           because of admissibility problems          --
                              structural induction
   --------------------------------------------------------------------------- *)
 
 Goal "! exA exB s t. \
 \ Forall (%x. x:act (A||B)) sch & \
-\ Filter (%a. a:act A)`sch << filter_act`exA  &\
-\ Filter (%a. a:act B)`sch << filter_act`exB \
-\ --> Filter_ex2 (asig_of A)`(ProjA2`(snd (mkex A B sch (s,exA) (t,exB)))) =   \
-\     Zip`(Filter (%a. a:act A)`sch)`(Map snd`exA)";
+\ Filter (%a. a:act A)$sch << filter_act$exA  &\
+\ Filter (%a. a:act B)$sch << filter_act$exB \
+\ --> Filter_ex2 (asig_of A)$(ProjA2$(snd (mkex A B sch (s,exA) (t,exB)))) =   \
+\     Zip$(Filter (%a. a:act A)$sch)$(Map snd$exA)";
 
 by (mkex_induct_tac "sch" "exB" "exA");
 
 qed"filter_mkex_is_exA_tmp";
 
 (*---------------------------------------------------------------------------
-                      zip`(proj1`y)`(proj2`y) = y   (using the lift operations)
+                      zip$(proj1$y)$(proj2$y) = y   (using the lift operations)
                     lemma for admissibility problems         
   --------------------------------------------------------------------------- *)
 
-Goal  "Zip`(Map fst`y)`(Map snd`y) = y";
+Goal  "Zip$(Map fst$y)$(Map snd$y) = y";
 by (Seq_induct_tac "y" [] 1);
 qed"Zip_Map_fst_snd";
 
 
 (*---------------------------------------------------------------------------
-      filter A`sch = proj1`ex   -->  zip`(filter A`sch)`(proj2`ex) = ex 
+      filter A$sch = proj1$ex   -->  zip$(filter A$sch)$(proj2$ex) = ex 
          lemma for eliminating non admissible equations in assumptions      
   --------------------------------------------------------------------------- *)
 
 Goal "!! sch ex. \
-\ Filter (%a. a:act AB)`sch = filter_act`ex  \
-\ ==> ex = Zip`(Filter (%a. a:act AB)`sch)`(Map snd`ex)";
+\ Filter (%a. a:act AB)$sch = filter_act$ex  \
+\ ==> ex = Zip$(Filter (%a. a:act AB)$sch)$(Map snd$ex)";
 by (asm_full_simp_tac (simpset() addsimps [filter_act_def]) 1);
 by (rtac (Zip_Map_fst_snd RS sym) 1);
 qed"trick_against_eq_in_ass";
@@ -371,8 +371,8 @@
 
 Goal "!!sch exA exB.\
 \ [| Forall (%a. a:act (A||B)) sch ; \
-\ Filter (%a. a:act A)`sch = filter_act`(snd exA)  ;\
-\ Filter (%a. a:act B)`sch = filter_act`(snd exB) |]\
+\ Filter (%a. a:act A)$sch = filter_act$(snd exA)  ;\
+\ Filter (%a. a:act B)$sch = filter_act$(snd exB) |]\
 \ ==> Filter_ex (asig_of A) (ProjA (mkex A B sch exA exB)) = exA";
 by (asm_full_simp_tac (simpset() addsimps [ProjA_def,Filter_ex_def]) 1);
 by (pair_tac "exA" 1);
@@ -388,7 +388,7 @@
 
 (*---------------------------------------------------------------------------
      Filter of mkex(sch,exA,exB) to B after projection onto B is exB 
-        --  using zip`(proj1`exB)`(proj2`exB) instead of exB    --
+        --  using zip$(proj1$exB)$(proj2$exB) instead of exB    --
         --           because of admissibility problems          --
                              structural induction
   --------------------------------------------------------------------------- *)
@@ -396,10 +396,10 @@
 
 Goal "! exA exB s t. \
 \ Forall (%x. x:act (A||B)) sch & \
-\ Filter (%a. a:act A)`sch << filter_act`exA  &\
-\ Filter (%a. a:act B)`sch << filter_act`exB \
-\ --> Filter_ex2 (asig_of B)`(ProjB2`(snd (mkex A B sch (s,exA) (t,exB)))) =   \
-\     Zip`(Filter (%a. a:act B)`sch)`(Map snd`exB)";
+\ Filter (%a. a:act A)$sch << filter_act$exA  &\
+\ Filter (%a. a:act B)$sch << filter_act$exB \
+\ --> Filter_ex2 (asig_of B)$(ProjB2$(snd (mkex A B sch (s,exA) (t,exB)))) =   \
+\     Zip$(Filter (%a. a:act B)$sch)$(Map snd$exB)";
 
 (* notice necessary change of arguments exA and exB *)
 by (mkex_induct_tac "sch" "exA" "exB");
@@ -415,8 +415,8 @@
 
 Goal "!!sch exA exB.\
 \ [| Forall (%a. a:act (A||B)) sch ; \
-\ Filter (%a. a:act A)`sch = filter_act`(snd exA)  ;\
-\ Filter (%a. a:act B)`sch = filter_act`(snd exB) |]\
+\ Filter (%a. a:act A)$sch = filter_act$(snd exA)  ;\
+\ Filter (%a. a:act B)$sch = filter_act$(snd exB) |]\
 \ ==> Filter_ex (asig_of B) (ProjB (mkex A B sch exA exB)) = exB";
 by (asm_full_simp_tac (simpset() addsimps [ProjB_def,Filter_ex_def]) 1);
 by (pair_tac "exA" 1);
@@ -436,8 +436,8 @@
 
 Goal "!s t exA exB. \
 \ Forall (%x. x : act (A || B)) sch &\
-\ Filter (%a. a:act A)`sch << filter_act`exA  &\
-\ Filter (%a. a:act B)`sch << filter_act`exB \
+\ Filter (%a. a:act A)$sch << filter_act$exA  &\
+\ Filter (%a. a:act B)$sch << filter_act$exB \
 \  --> Forall (%x. fst x : act (A ||B))   \
 \        (snd (mkex A B sch (s,exA) (t,exB)))";
 
@@ -453,8 +453,8 @@
 
 Goal  
 "sch : schedules (A||B) = \
-\ (Filter (%a. a:act A)`sch : schedules A &\
-\  Filter (%a. a:act B)`sch : schedules B &\
+\ (Filter (%a. a:act A)$sch : schedules A &\
+\  Filter (%a. a:act B)$sch : schedules B &\
 \  Forall (%x. x:act (A||B)) sch)";
 
 by (simp_tac (simpset() addsimps [schedules_def, has_schedule_def]) 1);
diff -r a7897aebbffc -r f4745d77e620 src/HOLCF/IOA/meta_theory/CompoScheds.thy
--- a/src/HOLCF/IOA/meta_theory/CompoScheds.thy	Tue Jan 09 15:32:27 2001 +0100
+++ b/src/HOLCF/IOA/meta_theory/CompoScheds.thy	Tue Jan 09 15:36:30 2001 +0100
@@ -26,10 +26,10 @@
 mkex_def  
   "mkex A B sch exA exB == 
        ((fst exA,fst exB),
-        (mkex2 A B`sch`(snd exA)`(snd exB)) (fst exA) (fst exB))"
+        (mkex2 A B$sch$(snd exA)$(snd exB)) (fst exA) (fst exB))"
 
 mkex2_def
-  "mkex2 A B == (fix`(LAM h sch exA exB. (%s t. case sch of 
+  "mkex2 A B == (fix$(LAM h sch exA exB. (%s t. case sch of 
        nil => nil
     | x##xs => 
       (case x of 
@@ -37,25 +37,25 @@
       | Def y => 
          (if y:act A then 
              (if y:act B then 
-                (case HD`exA of
+                (case HD$exA of
                    Undef => UU
-                 | Def a => (case HD`exB of
+                 | Def a => (case HD$exB of
                               Undef => UU
                             | Def b => 
                    (y,(snd a,snd b))>>
-                     (h`xs`(TL`exA)`(TL`exB)) (snd a) (snd b)))
+                     (h$xs$(TL$exA)$(TL$exB)) (snd a) (snd b)))
               else
-                (case HD`exA of
+                (case HD$exA of
                    Undef => UU
                  | Def a => 
-                   (y,(snd a,t))>>(h`xs`(TL`exA)`exB) (snd a) t)
+                   (y,(snd a,t))>>(h$xs$(TL$exA)$exB) (snd a) t)
               )
           else 
              (if y:act B then 
-                (case HD`exB of
+                (case HD$exB of
                    Undef => UU
                  | Def b => 
-                   (y,(s,snd b))>>(h`xs`exA`(TL`exB)) s (snd b))
+                   (y,(s,snd b))>>(h$xs$exA$(TL$exB)) s (snd b))
              else
                UU
              )
@@ -67,8 +67,8 @@
        let schA = fst SchedsA; sigA = snd SchedsA; 
            schB = fst SchedsB; sigB = snd SchedsB       
        in
-       (    {sch. Filter (%a. a:actions sigA)`sch : schA}
-        Int {sch. Filter (%a. a:actions sigB)`sch : schB}
+       (    {sch. Filter (%a. a:actions sigA)$sch : schA}
+        Int {sch. Filter (%a. a:actions sigB)$sch : schB}
         Int {sch. Forall (%x. x:(actions sigA Un actions sigB)) sch},
         asig_comp sigA sigB)"
 
diff -r a7897aebbffc -r f4745d77e620 src/HOLCF/IOA/meta_theory/CompoTraces.ML
--- a/src/HOLCF/IOA/meta_theory/CompoTraces.ML	Tue Jan 09 15:32:27 2001 +0100
+++ b/src/HOLCF/IOA/meta_theory/CompoTraces.ML	Tue Jan 09 15:36:30 2001 +0100
@@ -24,24 +24,24 @@
 \      | Def y => \
 \         (if y:act A then \
 \             (if y:act B then \ 
-\                   ((Takewhile (%a. a:int A)`schA) \
-\                         @@(Takewhile (%a. a:int B)`schB) \
-\                              @@(y>>(mksch A B`xs   \
-\                                       `(TL`(Dropwhile (%a. a:int A)`schA))  \
-\                                       `(TL`(Dropwhile (%a. a:int B)`schB))  \
+\                   ((Takewhile (%a. a:int A)$schA) \
+\                         @@(Takewhile (%a. a:int B)$schB) \
+\                              @@(y>>(mksch A B$xs   \
+\                                       $(TL$(Dropwhile (%a. a:int A)$schA))  \
+\                                       $(TL$(Dropwhile (%a. a:int B)$schB))  \
 \                    )))   \
 \              else  \
-\                 ((Takewhile (%a. a:int A)`schA)  \
-\                      @@ (y>>(mksch A B`xs  \
-\                              `(TL`(Dropwhile (%a. a:int A)`schA))  \
-\                              `schB)))  \
+\                 ((Takewhile (%a. a:int A)$schA)  \
+\                      @@ (y>>(mksch A B$xs  \
+\                              $(TL$(Dropwhile (%a. a:int A)$schA))  \
+\                              $schB)))  \
 \              )   \
 \          else    \
 \             (if y:act B then  \ 
-\                 ((Takewhile (%a. a:int B)`schB)  \
-\                       @@ (y>>(mksch A B`xs   \
-\                              `schA   \
-\                              `(TL`(Dropwhile (%a. a:int B)`schB))  \
+\                 ((Takewhile (%a. a:int B)$schB)  \
+\                       @@ (y>>(mksch A B$xs   \
+\                              $schA   \
+\                              $(TL$(Dropwhile (%a. a:int B)$schB))  \
 \                              )))  \
 \             else  \
 \               UU  \
@@ -50,21 +50,21 @@
 \       ))");
 
 
-Goal "mksch A B`UU`schA`schB = UU";
+Goal "mksch A B$UU$schA$schB = UU";
 by (stac mksch_unfold 1);
 by (Simp_tac 1);
 qed"mksch_UU";
 
-Goal "mksch A B`nil`schA`schB = nil";
+Goal "mksch A B$nil$schA$schB = nil";
 by (stac mksch_unfold 1);
 by (Simp_tac 1);
 qed"mksch_nil";
 
 Goal "[|x:act A;x~:act B|]  \
-\   ==> mksch A B`(x>>tr)`schA`schB = \
-\         (Takewhile (%a. a:int A)`schA) \
-\         @@ (x>>(mksch A B`tr`(TL`(Dropwhile (%a. a:int A)`schA)) \
-\                             `schB))";
+\   ==> mksch A B$(x>>tr)$schA$schB = \
+\         (Takewhile (%a. a:int A)$schA) \
+\         @@ (x>>(mksch A B$tr$(TL$(Dropwhile (%a. a:int A)$schA)) \
+\                             $schB))";
 by (rtac trans 1);
 by (stac mksch_unfold 1);
 by (asm_full_simp_tac (simpset() addsimps [Consq_def,If_and_if]) 1);
@@ -72,9 +72,9 @@
 qed"mksch_cons1";
 
 Goal "[|x~:act A;x:act B|] \
-\   ==> mksch A B`(x>>tr)`schA`schB = \
-\        (Takewhile (%a. a:int B)`schB)  \
-\         @@ (x>>(mksch A B`tr`schA`(TL`(Dropwhile (%a. a:int B)`schB))  \
+\   ==> mksch A B$(x>>tr)$schA$schB = \
+\        (Takewhile (%a. a:int B)$schB)  \
+\         @@ (x>>(mksch A B$tr$schA$(TL$(Dropwhile (%a. a:int B)$schB))  \
 \                            ))";
 by (rtac trans 1);
 by (stac mksch_unfold 1);
@@ -83,11 +83,11 @@
 qed"mksch_cons2";
 
 Goal "[|x:act A;x:act B|] \
-\   ==> mksch A B`(x>>tr)`schA`schB = \
-\            (Takewhile (%a. a:int A)`schA) \
-\         @@ ((Takewhile (%a. a:int B)`schB)  \
-\         @@ (x>>(mksch A B`tr`(TL`(Dropwhile (%a. a:int A)`schA)) \
-\                            `(TL`(Dropwhile (%a. a:int B)`schB))))  \
+\   ==> mksch A B$(x>>tr)$schA$schB = \
+\            (Takewhile (%a. a:int A)$schA) \
+\         @@ ((Takewhile (%a. a:int B)$schB)  \
+\         @@ (x>>(mksch A B$tr$(TL$(Dropwhile (%a. a:int A)$schA)) \
+\                            $(TL$(Dropwhile (%a. a:int B)$schB))))  \
 \             )";
 by (rtac trans 1);
 by (stac mksch_unfold 1);
@@ -148,7 +148,7 @@
 
 Goal "!!A B. compatible A B ==> \
 \   ! schA schB. Forall (%x. x:act (A||B)) tr \
-\   --> Forall (%x. x:act (A||B)) (mksch A B`tr`schA`schB)";
+\   --> Forall (%x. x:act (A||B)) (mksch A B$tr$schA$schB)";
 by (Seq_induct_tac "tr" [Forall_def,sforall_def,mksch_def] 1); 
 by (safe_tac set_cs);
 by (asm_full_simp_tac (simpset() addsimps [actions_of_par]) 1);
@@ -175,7 +175,7 @@
 
 Goal "!!A B. compatible B A  ==> \
 \   ! schA schB.  (Forall (%x. x:act B & x~:act A) tr \
-\   --> Forall (%x. x:act B & x~:act A) (mksch A B`tr`schA`schB))";
+\   --> Forall (%x. x:act B & x~:act A) (mksch A B$tr$schA$schB))";
 
 by (Seq_induct_tac "tr" [Forall_def,sforall_def,mksch_def] 1);
 by (safe_tac set_cs);
@@ -186,7 +186,7 @@
 
 Goal "!!A B. compatible A B ==> \
 \   ! schA schB.  (Forall (%x. x:act A & x~:act B) tr \
-\   --> Forall (%x. x:act A & x~:act B) (mksch A B`tr`schA`schB))";
+\   --> Forall (%x. x:act A & x~:act B) (mksch A B$tr$schA$schB))";
 
 by (Seq_induct_tac "tr" [Forall_def,sforall_def,mksch_def] 1);
 by (safe_tac set_cs);
@@ -201,10 +201,10 @@
 
 Goal "[| Finite tr; is_asig(asig_of A); is_asig(asig_of B) |] ==> \
 \   ! x y. Forall (%x. x:act A) x & Forall (%x. x:act B) y & \
-\          Filter (%a. a:ext A)`x = Filter (%a. a:act A)`tr & \
-\          Filter (%a. a:ext B)`y = Filter (%a. a:act B)`tr &\
+\          Filter (%a. a:ext A)$x = Filter (%a. a:act A)$tr & \
+\          Filter (%a. a:ext B)$y = Filter (%a. a:act B)$tr &\
 \          Forall (%x. x:ext (A||B)) tr \
-\          --> Finite (mksch A B`tr`x`y)";
+\          --> Finite (mksch A B$tr$x$y)";
 
 by (etac Seq_Finite_ind  1);
 by (Asm_full_simp_tac 1);
@@ -222,10 +222,10 @@
           [not_ext_is_int_or_not_act,FiniteConc]) 1);
 (* now for conclusion IH applicable, but assumptions have to be transformed *)
 by (dres_inst_tac [("x","x"),
-                   ("g","Filter (%a. a:act A)`s")] subst_lemma2 1);
+                   ("g","Filter (%a. a:act A)$s")] subst_lemma2 1);
 by (assume_tac 1);
 by (dres_inst_tac [("x","y"),
-                   ("g","Filter (%a. a:act B)`s")] subst_lemma2 1);
+                   ("g","Filter (%a. a:act B)$s")] subst_lemma2 1);
 by (assume_tac 1);
 (* IH *)
 by (asm_full_simp_tac (simpset()
@@ -240,7 +240,7 @@
           [not_ext_is_int_or_not_act,FiniteConc]) 1);
 (* now for conclusion IH applicable, but assumptions have to be transformed *)
 by (dres_inst_tac [("x","y"),
-                   ("g","Filter (%a. a:act B)`s")] subst_lemma2 1);
+                   ("g","Filter (%a. a:act B)$s")] subst_lemma2 1);
 by (assume_tac 1);
 (* IH *)
 by (asm_full_simp_tac (simpset()
@@ -255,7 +255,7 @@
           [not_ext_is_int_or_not_act,FiniteConc]) 1);
 (* now for conclusion IH applicable, but assumptions have to be transformed *)
 by (dres_inst_tac [("x","x"),
-                   ("g","Filter (%a. a:act A)`s")] subst_lemma2 1);
+                   ("g","Filter (%a. a:act A)$s")] subst_lemma2 1);
 by (assume_tac 1);
 (* IH *)
 by (asm_full_simp_tac (simpset()
@@ -274,11 +274,11 @@
 
 Goal " [| Finite bs; is_asig(asig_of A); is_asig(asig_of B);compatible A B|] ==>  \
 \! y. Forall (%x. x:act B) y & Forall (%x. x:act B & x~:act A) bs &\
-\    Filter (%a. a:ext B)`y = Filter (%a. a:act B)`(bs @@ z) \
-\    --> (? y1 y2.  (mksch A B`(bs @@ z)`x`y) = (y1 @@ (mksch A B`z`x`y2)) & \
+\    Filter (%a. a:ext B)$y = Filter (%a. a:act B)$(bs @@ z) \
+\    --> (? y1 y2.  (mksch A B$(bs @@ z)$x$y) = (y1 @@ (mksch A B$z$x$y2)) & \
 \                   Forall (%x. x:act B & x~:act A) y1 & \
 \                   Finite y1 & y = (y1 @@ y2) & \
-\                   Filter (%a. a:ext B)`y1 = bs)";
+\                   Filter (%a. a:ext B)$y1 = bs)";
 by (forw_inst_tac [("A1","A")] (compat_commute RS iffD1) 1);
 by (etac Seq_Finite_ind  1);
 by (REPEAT (rtac allI 1));
@@ -297,12 +297,12 @@
 by (REPEAT (etac conjE 1));
 (* transform assumption f eB y = f B (s@z) *)
 by (dres_inst_tac [("x","y"),
-                   ("g","Filter (%a. a:act B)`(s@@z)")] subst_lemma2 1);
+                   ("g","Filter (%a. a:act B)$(s@@z)")] subst_lemma2 1);
 by (assume_tac 1);
 Addsimps [FilterConc]; 
 by (asm_full_simp_tac (simpset() addsimps [not_ext_is_int_or_not_act]) 1);
 (* apply IH *)
-by (eres_inst_tac [("x","TL`(Dropwhile (%a. a:int B)`y)")] allE 1);
+by (eres_inst_tac [("x","TL$(Dropwhile (%a. a:int B)$y)")] allE 1);
 by (asm_full_simp_tac (simpset() addsimps [ForallTL,ForallDropwhile])1);
 by (REPEAT (etac exE 1));
 by (REPEAT (etac conjE 1));
@@ -311,7 +311,7 @@
 by (rotate_tac ~2 1); 
 by (Asm_full_simp_tac 1); 
 (* instantiate y1a and y2a *)
-by (res_inst_tac [("x","Takewhile (%a. a:int B)`y @@ a>>y1")] exI 1);
+by (res_inst_tac [("x","Takewhile (%a. a:int B)$y @@ a>>y1")] exI 1);
 by (res_inst_tac [("x","y2")] exI 1);
 (* elminate all obligations up to two depending on Conc_assoc *)
 by (asm_full_simp_tac (simpset() addsimps [ForallPTakewhileQ, intA_is_not_actB,
@@ -328,11 +328,11 @@
 
 Goal " [| Finite as; is_asig(asig_of A); is_asig(asig_of B);compatible A B|] ==>  \
 \! x. Forall (%x. x:act A) x & Forall (%x. x:act A & x~:act B) as &\
-\    Filter (%a. a:ext A)`x = Filter (%a. a:act A)`(as @@ z) \
-\    --> (? x1 x2.  (mksch A B`(as @@ z)`x`y) = (x1 @@ (mksch A B`z`x2`y)) & \
+\    Filter (%a. a:ext A)$x = Filter (%a. a:act A)$(as @@ z) \
+\    --> (? x1 x2.  (mksch A B$(as @@ z)$x$y) = (x1 @@ (mksch A B$z$x2$y)) & \
 \                   Forall (%x. x:act A & x~:act B) x1 & \
 \                   Finite x1 & x = (x1 @@ x2) & \
-\                   Filter (%a. a:ext A)`x1 = as)";
+\                   Filter (%a. a:ext A)$x1 = as)";
 by (forw_inst_tac [("A1","A")] (compat_commute RS iffD1) 1);
 by (etac Seq_Finite_ind  1);
 by (REPEAT (rtac allI 1));
@@ -351,12 +351,12 @@
 by (REPEAT (etac conjE 1));
 (* transform assumption f eA x = f A (s@z) *)
 by (dres_inst_tac [("x","x"),
-                   ("g","Filter (%a. a:act A)`(s@@z)")] subst_lemma2 1);
+                   ("g","Filter (%a. a:act A)$(s@@z)")] subst_lemma2 1);
 by (assume_tac 1);
 Addsimps [FilterConc]; 
 by (asm_full_simp_tac (simpset() addsimps [not_ext_is_int_or_not_act]) 1);
 (* apply IH *)
-by (eres_inst_tac [("x","TL`(Dropwhile (%a. a:int A)`x)")] allE 1);
+by (eres_inst_tac [("x","TL$(Dropwhile (%a. a:int A)$x)")] allE 1);
 by (asm_full_simp_tac (simpset() addsimps [ForallTL,ForallDropwhile])1);
 by (REPEAT (etac exE 1));
 by (REPEAT (etac conjE 1));
@@ -365,7 +365,7 @@
 by (rotate_tac ~2 1); 
 by (Asm_full_simp_tac 1); 
 (* instantiate y1a and y2a *)
-by (res_inst_tac [("x","Takewhile (%a. a:int A)`x @@ a>>x1")] exI 1);
+by (res_inst_tac [("x","Takewhile (%a. a:int A)$x @@ a>>x1")] exI 1);
 by (res_inst_tac [("x","x2")] exI 1);
 (* elminate all obligations up to two depending on Conc_assoc *)
 by (asm_full_simp_tac (simpset() addsimps [ForallPTakewhileQ, intA_is_not_actB,
@@ -380,7 +380,7 @@
 
 
 Goal "Finite y ==> ! z tr. Forall (%a.a:ext (A||B)) tr & \
-\                             y = z @@ mksch A B`tr`a`b\
+\                             y = z @@ mksch A B$tr$a$b\
 \                             --> Finite tr";
 by (etac Seq_Finite_ind  1);
 by Auto_tac;
@@ -422,7 +422,7 @@
 by (rotate_tac ~2 2);
 by (rotate_tac ~2 3);
 by (asm_full_simp_tac (HOL_basic_ss addsimps [mksch_cons3]) 2);
-by (eres_inst_tac [("x","sb@@Takewhile (%a. a: int A)`a @@ Takewhile (%a. a:int B)`b@@(aaa>>nil)")] allE 2);
+by (eres_inst_tac [("x","sb@@Takewhile (%a. a: int A)$a @@ Takewhile (%a. a:int B)$b@@(aaa>>nil)")] allE 2);
 by (eres_inst_tac [("x","sa")] allE 2);
 by (asm_full_simp_tac (simpset() addsimps [Conc_assoc])2);
 
@@ -455,7 +455,7 @@
 qed"FiniteConcUU";
 
 finiteR_mksch
-  "Finite (mksch A B`tr`x`y) --> Finite tr"
+  "Finite (mksch A B$tr$x$y) --> Finite tr"
 *)
 
 
@@ -470,9 +470,9 @@
 \           is_asig(asig_of A); is_asig(asig_of B) |] ==> \
 \ ! schA schB. Forall (%x. x:act A) schA & Forall (%x. x:act B) schB & \
 \ Forall (%x. x:ext (A||B)) tr & \
-\ Filter (%a. a:act A)`tr << Filter (%a. a:ext A)`schA &\
-\ Filter (%a. a:act B)`tr << Filter (%a. a:ext B)`schB  \
-\ --> Filter (%a. a:ext (A||B))`(mksch A B`tr`schA`schB) = tr";
+\ Filter (%a. a:act A)$tr << Filter (%a. a:ext A)$schA &\
+\ Filter (%a. a:act B)$tr << Filter (%a. a:ext B)$schB  \
+\ --> Filter (%a. a:ext (A||B))$(mksch A B$tr$schA$schB) = tr";
 
 by (Seq_induct_tac "tr" [Forall_def,sforall_def,mksch_def] 1);
 
@@ -546,10 +546,10 @@
 \ is_asig(asig_of A); is_asig(asig_of B) |] ==> \
 \ Forall (%x. x:ext (A||B)) tr & \
 \ Forall (%x. x:act A) schA & Forall (%x. x:act B) schB & \
-\ Filter (%a. a:ext A)`schA = Filter (%a. a:act A)`tr &\
-\ Filter (%a. a:ext B)`schB = Filter (%a. a:act B)`tr &\
+\ Filter (%a. a:ext A)$schA = Filter (%a. a:act A)$tr &\
+\ Filter (%a. a:ext B)$schB = Filter (%a. a:act B)$tr &\
 \ LastActExtsch A schA & LastActExtsch B schB  \
-\ --> Filter (%a. a:act A)`(mksch A B`tr`schA`schB) = schA";
+\ --> Filter (%a. a:act A)$(mksch A B$tr$schA$schB) = schA";
 
 by (res_inst_tac [("Q","%x. x:act B & x~:act A"),("x","tr")] take_lemma_less_induct 1);
 by (REPEAT (etac conjE 1));
@@ -600,7 +600,7 @@
 
 (* eliminate the B-only prefix *)
 
-by (subgoal_tac "(Filter (%a. a :act A)`y1) = nil" 1);
+by (subgoal_tac "(Filter (%a. a :act A)$y1) = nil" 1);
 by (etac ForallQFilterPnil 2);
 by (assume_tac 2);
 by (Fast_tac 2);
@@ -613,7 +613,7 @@
 by (rotate_tac ~2 1);
 by (Asm_full_simp_tac 1);
 
-by (subgoal_tac "Filter (%a. a:act A & a:ext B)`y1=nil" 1);
+by (subgoal_tac "Filter (%a. a:act A & a:ext B)$y1=nil" 1);
 by (rotate_tac ~1 1);
 by (Asm_full_simp_tac  1);
 (* eliminate introduced subgoal 2 *)
@@ -651,7 +651,7 @@
 by (asm_full_simp_tac (simpset() addsimps [ext_and_act]) 1);
 (* assumption schA *)
 by (dres_inst_tac [("x","schA"),
-                   ("g","Filter (%a. a:act A)`s2")] subst_lemma2 1);
+                   ("g","Filter (%a. a:act A)$s2")] subst_lemma2 1);
 by (assume_tac 1);
 by (Asm_full_simp_tac 1);
 (* assumptions concerning LastActExtsch, cannot be rewritten, as LastActExtsmalli are looping  *)
@@ -680,10 +680,10 @@
 \ is_asig(asig_of A); is_asig(asig_of B) |] ==> \
 \ Forall (%x. x:ext (A||B)) tr & \
 \ Forall (%x. x:act A) schA & Forall (%x. x:act B) schB & \
-\ Filter (%a. a:ext A)`schA = Filter (%a. a:act A)`tr &\
-\ Filter (%a. a:ext B)`schB = Filter (%a. a:act B)`tr &\
+\ Filter (%a. a:ext A)$schA = Filter (%a. a:act A)$tr &\
+\ Filter (%a. a:ext B)$schB = Filter (%a. a:act B)$tr &\
 \ LastActExtsch A schA & LastActExtsch B schB  \
-\ --> Filter (%a. a:act A)`(mksch A B`tr`schA`schB) = schA";
+\ --> Filter (%a. a:act A)$(mksch A B$tr$schA$schB) = schA";
 
 by (strip_tac 1);
 by (resolve_tac seq.take_lemmas 1);
@@ -756,7 +756,7 @@
 
 (* eliminate the B-only prefix *)
 
-by (subgoal_tac "(Filter (%a. a :act A)`y1) = nil" 1);
+by (subgoal_tac "(Filter (%a. a :act A)$y1) = nil" 1);
 by (etac ForallQFilterPnil 2);
 by (assume_tac 2);
 by (Fast_tac 2);
@@ -769,7 +769,7 @@
 by (rotate_tac ~2 1);
 by (Asm_full_simp_tac 1);
 
-by (subgoal_tac "Filter (%a. a:act A & a:ext B)`y1=nil" 1);
+by (subgoal_tac "Filter (%a. a:act A & a:ext B)$y1=nil" 1);
 by (rotate_tac ~1 1);
 by (Asm_full_simp_tac  1);
 (* eliminate introduced subgoal 2 *)
@@ -808,7 +808,7 @@
 by (REPEAT (etac conjE 1));
 (* assumption schA *)
 by (dres_inst_tac [("x","schA"),
-                   ("g","Filter (%a. a:act A)`rs")] subst_lemma2 1);
+                   ("g","Filter (%a. a:act A)$rs")] subst_lemma2 1);
 by (assume_tac 1);
 by (asm_full_simp_tac (simpset() addsimps [int_is_not_ext]) 1);
 (* assumptions concerning LastActExtsch, cannot be rewritten, as LastActExtsmalli are looping  *)
@@ -828,7 +828,7 @@
 by (rotate_tac ~2 1);
 by (Asm_full_simp_tac  1);
 
-by (subgoal_tac "Filter (%a. a:act A & a:ext B)`y1=nil" 1);
+by (subgoal_tac "Filter (%a. a:act A & a:ext B)$y1=nil" 1);
 by (rotate_tac ~1 1);
 by (Asm_full_simp_tac  1);
 (* eliminate introduced subgoal 2 *)
@@ -860,7 +860,7 @@
 by (REPEAT (etac conjE 1));
 (* assumption schA *)
 by (dres_inst_tac [("x","schA"),
-                   ("g","Filter (%a. a:act A)`rs")] subst_lemma2 1);
+                   ("g","Filter (%a. a:act A)$rs")] subst_lemma2 1);
 by (assume_tac 1);
 by (asm_full_simp_tac (simpset() addsimps [int_is_not_ext]) 1);
 
@@ -878,7 +878,7 @@
 
 (* assumption schB *)
 by (dres_inst_tac [("x","y2"),
-                   ("g","Filter (%a. a:act B)`rs")] subst_lemma2 1);
+                   ("g","Filter (%a. a:act B)$rs")] subst_lemma2 1);
 by (assume_tac 1);
 by (asm_full_simp_tac (simpset() addsimps [intA_is_not_actB,int_is_not_ext]) 1);
 
@@ -920,10 +920,10 @@
 \ is_asig(asig_of A); is_asig(asig_of B) |] ==> \
 \ Forall (%x. x:ext (A||B)) tr & \
 \ Forall (%x. x:act A) schA & Forall (%x. x:act B) schB & \
-\ Filter (%a. a:ext A)`schA = Filter (%a. a:act A)`tr &\
-\ Filter (%a. a:ext B)`schB = Filter (%a. a:act B)`tr &\
+\ Filter (%a. a:ext A)$schA = Filter (%a. a:act A)$tr &\
+\ Filter (%a. a:ext B)$schB = Filter (%a. a:act B)$tr &\
 \ LastActExtsch A schA & LastActExtsch B schB  \
-\ --> Filter (%a. a:act B)`(mksch A B`tr`schA`schB) = schB";
+\ --> Filter (%a. a:act B)$(mksch A B$tr$schA$schB) = schB";
 
 by (strip_tac 1);
 by (resolve_tac seq.take_lemmas 1);
@@ -998,7 +998,7 @@
 
 (* eliminate the A-only prefix *)
 
-by (subgoal_tac "(Filter (%a. a :act B)`x1) = nil" 1);
+by (subgoal_tac "(Filter (%a. a :act B)$x1) = nil" 1);
 by (etac ForallQFilterPnil 2);
 by (assume_tac 2);
 by (Fast_tac 2);
@@ -1011,7 +1011,7 @@
 by (rotate_tac ~2 1);
 by (Asm_full_simp_tac 1);
 
-by (subgoal_tac "Filter (%a. a:act B & a:ext A)`x1=nil" 1);
+by (subgoal_tac "Filter (%a. a:act B & a:ext A)$x1=nil" 1);
 by (rotate_tac ~1 1);
 by (Asm_full_simp_tac  1);
 (* eliminate introduced subgoal 2 *)
@@ -1050,7 +1050,7 @@
 by (REPEAT (etac conjE 1));
 (* assumption schB *)
 by (dres_inst_tac [("x","schB"),
-                   ("g","Filter (%a. a:act B)`rs")] subst_lemma2 1);
+                   ("g","Filter (%a. a:act B)$rs")] subst_lemma2 1);
 by (assume_tac 1);
 by (asm_full_simp_tac (simpset() addsimps [int_is_not_ext]) 1);
 (* assumptions concerning LastActExtsch, cannot be rewritten, as LastActExtsmalli are looping  *)
@@ -1070,7 +1070,7 @@
 by (rotate_tac ~2 1);
 by (Asm_full_simp_tac  1);
 
-by (subgoal_tac "Filter (%a. a:act B & a:ext A)`x1=nil" 1);
+by (subgoal_tac "Filter (%a. a:act B & a:ext A)$x1=nil" 1);
 by (rotate_tac ~1 1);
 by (Asm_full_simp_tac  1);
 (* eliminate introduced subgoal 2 *)
@@ -1102,7 +1102,7 @@
 by (REPEAT (etac conjE 1));
 (* assumption schA *)
 by (dres_inst_tac [("x","schB"),
-                   ("g","Filter (%a. a:act B)`rs")] subst_lemma2 1);
+                   ("g","Filter (%a. a:act B)$rs")] subst_lemma2 1);
 by (assume_tac 1);
 by (asm_full_simp_tac (simpset() addsimps [int_is_not_ext]) 1);
 
@@ -1120,7 +1120,7 @@
 
 (* assumption schA *)
 by (dres_inst_tac [("x","x2"),
-                   ("g","Filter (%a. a:act A)`rs")] subst_lemma2 1);
+                   ("g","Filter (%a. a:act A)$rs")] subst_lemma2 1);
 by (assume_tac 1);
 by (asm_full_simp_tac (simpset() addsimps [intA_is_not_actB,int_is_not_ext]) 1);
 
@@ -1158,8 +1158,8 @@
 "!! A B. [| is_trans_of A; is_trans_of B; compatible A B; compatible B A; \
 \           is_asig(asig_of A); is_asig(asig_of B)|] \
 \       ==>  tr: traces(A||B) = \
-\            (Filter (%a. a:act A)`tr : traces A &\
-\             Filter (%a. a:act B)`tr : traces B &\
+\            (Filter (%a. a:act A)$tr : traces A &\
+\             Filter (%a. a:act B)$tr : traces B &\
 \             Forall (%x. x:ext(A||B)) tr)";
 
 by (simp_tac (simpset() addsimps [traces_def,has_trace_def]) 1);
@@ -1167,12 +1167,12 @@
  
 (* ==> *) 
 (* There is a schedule of A *)
-by (res_inst_tac [("x","Filter (%a. a:act A)`sch")] bexI 1);
+by (res_inst_tac [("x","Filter (%a. a:act A)$sch")] bexI 1);
 by (asm_full_simp_tac (simpset() addsimps [compositionality_sch]) 2);
 by (asm_full_simp_tac (simpset() addsimps [compatibility_consequence1,
                   externals_of_par,ext1_ext2_is_not_act1]) 1);
 (* There is a schedule of B *)
-by (res_inst_tac [("x","Filter (%a. a:act B)`sch")] bexI 1);
+by (res_inst_tac [("x","Filter (%a. a:act B)$sch")] bexI 1);
 by (asm_full_simp_tac (simpset() addsimps [compositionality_sch]) 2);
 by (asm_full_simp_tac (simpset() addsimps [compatibility_consequence2,
                   externals_of_par,ext1_ext2_is_not_act2]) 1);
@@ -1197,7 +1197,7 @@
 ren "h1 h2 schA schB" 1;
 (* mksch is exactly the construction of trA||B out of schA, schB, and the oracle tr,
    we need here *)
-by (res_inst_tac [("x","mksch A B`tr`schA`schB")] bexI 1);
+by (res_inst_tac [("x","mksch A B$tr$schA$schB")] bexI 1);
 
 (* External actions of mksch are just the oracle *)
 by (asm_full_simp_tac (simpset() addsimps [FilterA_mksch_is_tr RS spec RS spec RS mp]) 1);
diff -r a7897aebbffc -r f4745d77e620 src/HOLCF/IOA/meta_theory/CompoTraces.thy
--- a/src/HOLCF/IOA/meta_theory/CompoTraces.thy	Tue Jan 09 15:32:27 2001 +0100
+++ b/src/HOLCF/IOA/meta_theory/CompoTraces.thy	Tue Jan 09 15:36:30 2001 +0100
@@ -17,7 +17,7 @@
 defs
 
 mksch_def
-  "mksch A B == (fix`(LAM h tr schA schB. case tr of 
+  "mksch A B == (fix$(LAM h tr schA schB. case tr of 
        nil => nil
     | x##xs => 
       (case x of 
@@ -25,24 +25,24 @@
       | Def y => 
          (if y:act A then 
              (if y:act B then 
-                   ((Takewhile (%a. a:int A)`schA)
-                      @@ (Takewhile (%a. a:int B)`schB)
-                           @@ (y>>(h`xs
-                                    `(TL`(Dropwhile (%a. a:int A)`schA))
-                                    `(TL`(Dropwhile (%a. a:int B)`schB))
+                   ((Takewhile (%a. a:int A)$schA)
+                      @@ (Takewhile (%a. a:int B)$schB)
+                           @@ (y>>(h$xs
+                                    $(TL$(Dropwhile (%a. a:int A)$schA))
+                                    $(TL$(Dropwhile (%a. a:int B)$schB))
                     )))
               else
-                 ((Takewhile (%a. a:int A)`schA)
-                  @@ (y>>(h`xs
-                           `(TL`(Dropwhile (%a. a:int A)`schA))
-                           `schB)))
+                 ((Takewhile (%a. a:int A)$schA)
+                  @@ (y>>(h$xs
+                           $(TL$(Dropwhile (%a. a:int A)$schA))
+                           $schB)))
               )
           else 
              (if y:act B then 
-                 ((Takewhile (%a. a:int B)`schB)
-                     @@ (y>>(h`xs
-                              `schA
-                              `(TL`(Dropwhile (%a. a:int B)`schB))
+                 ((Takewhile (%a. a:int B)$schB)
+                     @@ (y>>(h$xs
+                              $schA
+                              $(TL$(Dropwhile (%a. a:int B)$schB))
                               )))
              else
                UU
@@ -56,8 +56,8 @@
        let trA = fst TracesA; sigA = snd TracesA; 
            trB = fst TracesB; sigB = snd TracesB       
        in
-       (    {tr. Filter (%a. a:actions sigA)`tr : trA}
-        Int {tr. Filter (%a. a:actions sigB)`tr : trB}
+       (    {tr. Filter (%a. a:actions sigA)$tr : trA}
+        Int {tr. Filter (%a. a:actions sigB)$tr : trB}
         Int {tr. Forall (%x. x:(externals sigA Un externals sigB)) tr},
         asig_comp sigA sigB)"
 
@@ -65,7 +65,7 @@
 
 
 finiteR_mksch
-  "Finite (mksch A B`tr`x`y) --> Finite tr"
+  "Finite (mksch A B$tr$x$y) --> Finite tr"
 
 
 
diff -r a7897aebbffc -r f4745d77e620 src/HOLCF/IOA/meta_theory/Compositionality.ML
--- a/src/HOLCF/IOA/meta_theory/Compositionality.ML	Tue Jan 09 15:32:27 2001 +0100
+++ b/src/HOLCF/IOA/meta_theory/Compositionality.ML	Tue Jan 09 15:36:30 2001 +0100
@@ -15,9 +15,9 @@
 
 Goal 
 "!! A B. [| compatible A B; Forall (%a. a: ext A | a: ext B) tr |] ==> \
-\           Filter (%a. a: act A)`tr= Filter (%a. a: ext A)`tr";
+\           Filter (%a. a: act A)$tr= Filter (%a. a: ext A)$tr";
 by (rtac ForallPFilterQR 1);
-(* i.e.: [| (! x. P x --> (Q x = R x)) ; Forall P tr |] ==> Filter Q`tr = Filter R`tr *)
+(* i.e.: [| (! x. P x --> (Q x = R x)) ; Forall P tr |] ==> Filter Q$tr = Filter R$tr *)
 by (assume_tac 2);
 by (rtac compatibility_consequence3 1);
 by (REPEAT (asm_full_simp_tac (simpset() 
@@ -32,7 +32,7 @@
 qed"compatibility_consequence4";
 
 Goal "[| compatible A B; Forall (%a. a: ext B | a: ext A) tr |] ==> \
-\           Filter (%a. a: act A)`tr= Filter (%a. a: ext A)`tr";
+\           Filter (%a. a: act A)$tr= Filter (%a. a: ext A)$tr";
 by (rtac ForallPFilterQR 1);
 by (assume_tac 2);
 by (rtac compatibility_consequence4 1);
diff -r a7897aebbffc -r f4745d77e620 src/HOLCF/IOA/meta_theory/Deadlock.ML
--- a/src/HOLCF/IOA/meta_theory/Deadlock.ML	Tue Jan 09 15:32:27 2001 +0100
+++ b/src/HOLCF/IOA/meta_theory/Deadlock.ML	Tue Jan 09 15:36:30 2001 +0100
@@ -10,8 +10,8 @@
                input actions may always be added to a schedule
 **********************************************************************************)
 
-Goal "[| Filter (%x. x:act A)`sch : schedules A; a:inp A; input_enabled A; Finite sch|] \
-\         ==> Filter (%x. x:act A)`sch @@ a>>nil : schedules A";
+Goal "[| Filter (%x. x:act A)$sch : schedules A; a:inp A; input_enabled A; Finite sch|] \
+\         ==> Filter (%x. x:act A)$sch @@ a>>nil : schedules A";
 by (asm_full_simp_tac (simpset() addsimps [schedules_def,has_schedule_def]) 1);
 by (safe_tac set_cs);
 by (ftac inp_is_act 1);
@@ -21,7 +21,7 @@
 by (subgoal_tac "Finite ex" 1);
 by (asm_full_simp_tac (simpset() addsimps [filter_act_def]) 2);
 by (rtac (Map2Finite RS iffD1) 2);
-by (res_inst_tac [("t","Map fst`ex")] subst 2);
+by (res_inst_tac [("t","Map fst$ex")] subst 2);
 by (assume_tac 2);
 by (etac FiniteFilter 2);
 (* subgoal 1 *)
@@ -52,7 +52,7 @@
 **********************************************************************************)
 Delsplits [split_if];
 Goal "[| a : local A; Finite sch; sch : schedules (A||B); \
-\            Filter (%x. x:act A)`(sch @@ a>>nil) : schedules A; compatible A B; input_enabled B |] \
+\            Filter (%x. x:act A)$(sch @@ a>>nil) : schedules A; compatible A B; input_enabled B |] \
 \          ==> (sch @@ a>>nil) : schedules (A||B)";
 
 by (asm_full_simp_tac (simpset() addsimps [compositionality_sch,locals_def]) 1);
diff -r a7897aebbffc -r f4745d77e620 src/HOLCF/IOA/meta_theory/LiveIOA.thy
--- a/src/HOLCF/IOA/meta_theory/LiveIOA.thy	Tue Jan 09 15:32:27 2001 +0100
+++ b/src/HOLCF/IOA/meta_theory/LiveIOA.thy	Tue Jan 09 15:36:30 2001 +0100
@@ -45,7 +45,7 @@
    "liveexecutions AP == {exec. exec : executions (fst AP) & (exec |== (snd AP))}"
 
 livetraces_def
-  "livetraces AP == {mk_trace (fst AP)`(snd ex) | ex. ex:liveexecutions AP}"
+  "livetraces AP == {mk_trace (fst AP)$(snd ex) | ex. ex:liveexecutions AP}"
 
 live_implements_def
   "live_implements CL AM == (inp (fst CL) = inp (fst AM)) & 
diff -r a7897aebbffc -r f4745d77e620 src/HOLCF/IOA/meta_theory/RefCorrectness.ML
--- a/src/HOLCF/IOA/meta_theory/RefCorrectness.ML	Tue Jan 09 15:32:27 2001 +0100
+++ b/src/HOLCF/IOA/meta_theory/RefCorrectness.ML	Tue Jan 09 15:36:30 2001 +0100
@@ -21,8 +21,8 @@
 Goal "corresp_exC A f  = (LAM ex. (%s. case ex of \
 \      nil =>  nil   \
 \    | x##xs => (flift1 (%pr. (@cex. move A cex (f s) (fst pr) (f (snd pr)))   \
-\                              @@ ((corresp_exC A f `xs) (snd pr)))   \
-\                        `x) ))";
+\                              @@ ((corresp_exC A f $xs) (snd pr)))   \
+\                        $x) ))";
 by (rtac trans 1);
 by (rtac fix_eq2 1);
 by (rtac corresp_exC_def 1);
@@ -30,19 +30,19 @@
 by (simp_tac (simpset() addsimps [flift1_def]) 1);
 qed"corresp_exC_unfold";
 
-Goal "(corresp_exC A f`UU) s=UU";
+Goal "(corresp_exC A f$UU) s=UU";
 by (stac corresp_exC_unfold 1);
 by (Simp_tac 1);
 qed"corresp_exC_UU";
 
-Goal "(corresp_exC A f`nil) s = nil";
+Goal "(corresp_exC A f$nil) s = nil";
 by (stac corresp_exC_unfold 1);
 by (Simp_tac 1);
 qed"corresp_exC_nil";
 
-Goal "(corresp_exC A f`(at>>xs)) s = \
+Goal "(corresp_exC A f$(at>>xs)) s = \
 \          (@cex. move A cex (f s) (fst at) (f (snd at)))  \
-\          @@ ((corresp_exC A f`xs) (snd at))";
+\          @@ ((corresp_exC A f$xs) (snd at))";
 by (rtac trans 1);
 by (stac corresp_exC_unfold 1);
 by (asm_full_simp_tac (simpset() addsimps [Consq_def,flift1_def]) 1);
@@ -98,7 +98,7 @@
 
 Goal
    "[|is_ref_map f C A; reachable C s; (s,a,t):trans_of C|] ==>\
-\     mk_trace A`((@x. move A x (f s) a (f t))) = \
+\     mk_trace A$((@x. move A x (f s) a (f t))) = \
 \       (if a:ext A then a>>nil else nil)";
 
 by (cut_inst_tac [] move_is_move 1);
@@ -119,7 +119,7 @@
 (* --------------------------------------------------- *)
 
 
-Goal "mk_trace C`(ex1 @@ ex2)= (mk_trace C`ex1) @@ (mk_trace C`ex2)";
+Goal "mk_trace C$(ex1 @@ ex2)= (mk_trace C$ex1) @@ (mk_trace C$ex2)";
 by (simp_tac (simpset() addsimps [mk_trace_def,filter_act_def,
                                  FilterConc,MapConc]) 1);
 qed"mk_traceConc";
@@ -133,7 +133,7 @@
 Goalw [corresp_ex_def]
   "[|is_ref_map f C A; ext C = ext A|] ==>  \     
 \        !s. reachable C s & is_exec_frag C (s,xs) --> \
-\            mk_trace C`xs = mk_trace A`(snd (corresp_ex A f (s,xs)))";
+\            mk_trace C$xs = mk_trace A$(snd (corresp_ex A f (s,xs)))";
 
 by (pair_induct_tac "xs" [is_exec_frag_def] 1);
 (* cons case *) 
diff -r a7897aebbffc -r f4745d77e620 src/HOLCF/IOA/meta_theory/RefCorrectness.thy
--- a/src/HOLCF/IOA/meta_theory/RefCorrectness.thy	Tue Jan 09 15:32:27 2001 +0100
+++ b/src/HOLCF/IOA/meta_theory/RefCorrectness.thy	Tue Jan 09 15:36:30 2001 +0100
@@ -20,15 +20,15 @@
 defs
 
 corresp_ex_def
-  "corresp_ex A f ex == (f (fst ex),(corresp_exC A f`(snd ex)) (fst ex))"
+  "corresp_ex A f ex == (f (fst ex),(corresp_exC A f$(snd ex)) (fst ex))"
 
 
 corresp_exC_def
-  "corresp_exC A f  == (fix`(LAM h ex. (%s. case ex of 
+  "corresp_exC A f  == (fix$(LAM h ex. (%s. case ex of 
       nil =>  nil
     | x##xs => (flift1 (%pr. (@cex. move A cex (f s) (fst pr) (f (snd pr)))
-                              @@ ((h`xs) (snd pr)))
-                        `x) )))"
+                              @@ ((h$xs) (snd pr)))
+                        $x) )))"
  
 is_fair_ref_map_def
   "is_fair_ref_map f C A == 
diff -r a7897aebbffc -r f4745d77e620 src/HOLCF/IOA/meta_theory/RefMappings.thy
--- a/src/HOLCF/IOA/meta_theory/RefMappings.thy	Tue Jan 09 15:32:27 2001 +0100
+++ b/src/HOLCF/IOA/meta_theory/RefMappings.thy	Tue Jan 09 15:36:30 2001 +0100
@@ -24,7 +24,7 @@
   "move ioa ex s a t ==    
     (is_exec_frag ioa (s,ex) &  Finite ex & 
      laststate (s,ex)=t  &     
-     mk_trace ioa`ex = (if a:ext(ioa) then a>>nil else nil))"
+     mk_trace ioa$ex = (if a:ext(ioa) then a>>nil else nil))"
 
 is_ref_map_def
   "is_ref_map f C A ==                          
diff -r a7897aebbffc -r f4745d77e620 src/HOLCF/IOA/meta_theory/Seq.ML
--- a/src/HOLCF/IOA/meta_theory/Seq.ML	Tue Jan 09 15:32:27 2001 +0100
+++ b/src/HOLCF/IOA/meta_theory/Seq.ML	Tue Jan 09 15:36:30 2001 +0100
@@ -34,20 +34,20 @@
 bind_thm ("smap_unfold", fix_prover2 thy smap_def 
    "smap = (LAM f tr. case tr of  \
  \                         nil  => nil \
- \                       | x##xs => f`x ## smap`f`xs)");
+ \                       | x##xs => f$x ## smap$f$xs)");
 
-Goal "smap`f`nil=nil"; 
+Goal "smap$f$nil=nil"; 
 by (stac smap_unfold 1);
 by (Simp_tac 1);
 qed"smap_nil";
 
-Goal "smap`f`UU=UU"; 
+Goal "smap$f$UU=UU"; 
 by (stac smap_unfold 1);
 by (Simp_tac 1);
 qed"smap_UU";
 
 Goal 
-"[|x~=UU|] ==> smap`f`(x##xs)= (f`x)##smap`f`xs"; 
+"[|x~=UU|] ==> smap$f$(x##xs)= (f$x)##smap$f$xs"; 
 by (rtac trans 1);
 by (stac smap_unfold 1);
 by (Asm_full_simp_tac 1);
@@ -61,21 +61,21 @@
 bind_thm ("sfilter_unfold", fix_prover2 thy sfilter_def 
   "sfilter = (LAM P tr. case tr of  \
  \         nil   => nil \
- \       | x##xs => If P`x then x##(sfilter`P`xs) else sfilter`P`xs fi)");
+ \       | x##xs => If P$x then x##(sfilter$P$xs) else sfilter$P$xs fi)");
 
-Goal "sfilter`P`nil=nil";
+Goal "sfilter$P$nil=nil";
 by (stac sfilter_unfold 1);
 by (Simp_tac 1);
 qed"sfilter_nil";
 
-Goal "sfilter`P`UU=UU";
+Goal "sfilter$P$UU=UU";
 by (stac sfilter_unfold 1);
 by (Simp_tac 1);
 qed"sfilter_UU";
 
 Goal 
-"x~=UU ==> sfilter`P`(x##xs)=   \
-\             (If P`x then x##(sfilter`P`xs) else sfilter`P`xs fi)";
+"x~=UU ==> sfilter$P$(x##xs)=   \
+\             (If P$x then x##(sfilter$P$xs) else sfilter$P$xs fi)";
 by (rtac trans 1);
 by (stac sfilter_unfold 1);
 by (Asm_full_simp_tac 1);
@@ -89,20 +89,20 @@
 bind_thm ("sforall2_unfold", fix_prover2 thy sforall2_def 
    "sforall2 = (LAM P tr. case tr of  \
  \                         nil   => TT \
- \                       | x##xs => (P`x andalso sforall2`P`xs))");
+ \                       | x##xs => (P$x andalso sforall2$P$xs))");
 
-Goal "sforall2`P`nil=TT"; 
+Goal "sforall2$P$nil=TT"; 
 by (stac sforall2_unfold 1);
 by (Simp_tac 1);
 qed"sforall2_nil";
 
-Goal "sforall2`P`UU=UU"; 
+Goal "sforall2$P$UU=UU"; 
 by (stac sforall2_unfold 1);
 by (Simp_tac 1);
 qed"sforall2_UU";
 
 Goal 
-"x~=UU ==> sforall2`P`(x##xs)= ((P`x) andalso sforall2`P`xs)";
+"x~=UU ==> sforall2$P$(x##xs)= ((P$x) andalso sforall2$P$xs)";
 by (rtac trans 1);
 by (stac sforall2_unfold 1);
 by (Asm_full_simp_tac 1);
@@ -118,21 +118,21 @@
 bind_thm ("stakewhile_unfold", fix_prover2 thy stakewhile_def 
    "stakewhile = (LAM P tr. case tr of  \
  \                         nil   => nil \
- \                       | x##xs => (If P`x then x##(stakewhile`P`xs) else nil fi))");
+ \                       | x##xs => (If P$x then x##(stakewhile$P$xs) else nil fi))");
 
-Goal "stakewhile`P`nil=nil"; 
+Goal "stakewhile$P$nil=nil"; 
 by (stac stakewhile_unfold 1);
 by (Simp_tac 1);
 qed"stakewhile_nil";
 
-Goal "stakewhile`P`UU=UU"; 
+Goal "stakewhile$P$UU=UU"; 
 by (stac stakewhile_unfold 1);
 by (Simp_tac 1);
 qed"stakewhile_UU";
 
 Goal 
-"x~=UU ==> stakewhile`P`(x##xs) =   \
-\             (If P`x then x##(stakewhile`P`xs) else nil fi)";
+"x~=UU ==> stakewhile$P$(x##xs) =   \
+\             (If P$x then x##(stakewhile$P$xs) else nil fi)";
 by (rtac trans 1);
 by (stac stakewhile_unfold 1);
 by (Asm_full_simp_tac 1);
@@ -147,21 +147,21 @@
 bind_thm ("sdropwhile_unfold", fix_prover2 thy sdropwhile_def 
    "sdropwhile = (LAM P tr. case tr of  \
  \                         nil   => nil \
- \                       | x##xs => (If P`x then sdropwhile`P`xs else tr fi))");
+ \                       | x##xs => (If P$x then sdropwhile$P$xs else tr fi))");
 
-Goal "sdropwhile`P`nil=nil"; 
+Goal "sdropwhile$P$nil=nil"; 
 by (stac sdropwhile_unfold 1);
 by (Simp_tac 1);
 qed"sdropwhile_nil";
 
-Goal "sdropwhile`P`UU=UU"; 
+Goal "sdropwhile$P$UU=UU"; 
 by (stac sdropwhile_unfold 1);
 by (Simp_tac 1);
 qed"sdropwhile_UU";
 
 Goal 
-"x~=UU ==> sdropwhile`P`(x##xs) =   \
-\             (If P`x then sdropwhile`P`xs else x##xs fi)";
+"x~=UU ==> sdropwhile$P$(x##xs) =   \
+\             (If P$x then sdropwhile$P$xs else x##xs fi)";
 by (rtac trans 1);
 by (stac sdropwhile_unfold 1);
 by (Asm_full_simp_tac 1);
@@ -177,21 +177,21 @@
 bind_thm ("slast_unfold", fix_prover2 thy slast_def 
    "slast = (LAM tr. case tr of  \
  \                         nil   => UU \
- \                       | x##xs => (If is_nil`xs then x else slast`xs fi))");
+ \                       | x##xs => (If is_nil$xs then x else slast$xs fi))");
 
 
-Goal "slast`nil=UU"; 
+Goal "slast$nil=UU"; 
 by (stac slast_unfold 1);
 by (Simp_tac 1);
 qed"slast_nil";
 
-Goal "slast`UU=UU"; 
+Goal "slast$UU=UU"; 
 by (stac slast_unfold 1);
 by (Simp_tac 1);
 qed"slast_UU";
 
 Goal 
-"x~=UU ==> slast`(x##xs)= (If is_nil`xs then x else slast`xs fi)";
+"x~=UU ==> slast$(x##xs)= (If is_nil$xs then x else slast$xs fi)";
 by (rtac trans 1);
 by (stac slast_unfold 1);
 by (Asm_full_simp_tac 1);
@@ -237,19 +237,19 @@
 bind_thm ("sflat_unfold", fix_prover2 thy sflat_def 
    "sflat = (LAM tr. case tr of  \
  \                         nil   => nil \
- \                       | x##xs => x @@ sflat`xs)");
+ \                       | x##xs => x @@ sflat$xs)");
 
-Goal "sflat`nil=nil"; 
+Goal "sflat$nil=nil"; 
 by (stac sflat_unfold 1);
 by (Simp_tac 1);
 qed"sflat_nil";
 
-Goal "sflat`UU=UU"; 
+Goal "sflat$UU=UU"; 
 by (stac sflat_unfold 1);
 by (Simp_tac 1);
 qed"sflat_UU";
 
-Goal "sflat`(x##xs)= x@@(sflat`xs)"; 
+Goal "sflat$(x##xs)= x@@(sflat$xs)"; 
 by (rtac trans 1);
 by (stac sflat_unfold 1);
 by (Asm_full_simp_tac 1);
@@ -269,32 +269,32 @@
 \               nil   => nil    \
 \             | x##xs => (case t2 of     \
 \                          nil => UU    \
-\                        | y##ys => <x,y>##(szip`xs`ys)))");
+\                        | y##ys => <x,y>##(szip$xs$ys)))");
 
-Goal "szip`nil`y=nil"; 
+Goal "szip$nil$y=nil"; 
 by (stac szip_unfold 1);
 by (Simp_tac 1);
 qed"szip_nil";
 
-Goal "szip`UU`y=UU"; 
+Goal "szip$UU$y=UU"; 
 by (stac szip_unfold 1);
 by (Simp_tac 1);
 qed"szip_UU1";
 
-Goal "x~=nil ==> szip`x`UU=UU"; 
+Goal "x~=nil ==> szip$x$UU=UU"; 
 by (stac szip_unfold 1);
 by (Asm_full_simp_tac 1);
 by (res_inst_tac [("x","x")] seq.casedist 1);
 by (REPEAT (Asm_full_simp_tac 1));
 qed"szip_UU2";
 
-Goal "x~=UU ==> szip`(x##xs)`nil=UU";
+Goal "x~=UU ==> szip$(x##xs)$nil=UU";
 by (rtac trans 1);
 by (stac szip_unfold 1);
 by (REPEAT (Asm_full_simp_tac 1));
 qed"szip_cons_nil";
 
-Goal "[| x~=UU; y~=UU|] ==> szip`(x##xs)`(y##ys) = <x,y>##szip`xs`ys";
+Goal "[| x~=UU; y~=UU|] ==> szip$(x##xs)$(y##ys) = <x,y>##szip$xs$ys";
 by (rtac trans 1);
 by (stac szip_unfold 1);
 by (REPEAT (Asm_full_simp_tac 1));
@@ -348,7 +348,7 @@
 Addsimps [if_and_sconc];
 
 
-Goal "sfilter`P`(x @@ y) = (sfilter`P`x @@ sfilter`P`y)";
+Goal "sfilter$P$(x @@ y) = (sfilter$P$x @@ sfilter$P$y)";
 
 by (res_inst_tac[("x","x")] seq.ind 1);
 (* adm *)
@@ -360,7 +360,7 @@
 by (asm_full_simp_tac (simpset() setloop split_If_tac) 1);
 qed"sfiltersconc";
 
-Goal "sforall P (stakewhile`P`x)";
+Goal "sforall P (stakewhile$P$x)";
 by (simp_tac (simpset() addsimps [sforall_def]) 1);
 by (res_inst_tac[("x","x")] seq.ind 1);
 (* adm *)
@@ -372,7 +372,7 @@
 by (asm_full_simp_tac (simpset() setloop split_If_tac) 1);
 qed"sforallPstakewhileP";
 
-Goal "sforall P (sfilter`P`x)";
+Goal "sforall P (sfilter$P$x)";
 by (simp_tac (simpset() addsimps [sforall_def]) 1);
 by (res_inst_tac[("x","x")] seq.ind 1);
 (* adm *)
@@ -438,7 +438,7 @@
 
 
 qed_goalw "seq_finite_ind_lemma" thy  [seq.finite_def]
-"(!!n. P(seq_take n`s)) ==>  seq_finite(s) -->P(s)"
+"(!!n. P(seq_take n$s)) ==>  seq_finite(s) -->P(s)"
  (fn prems =>
         [
         (strip_tac 1),
diff -r a7897aebbffc -r f4745d77e620 src/HOLCF/IOA/meta_theory/Seq.thy
--- a/src/HOLCF/IOA/meta_theory/Seq.thy	Tue Jan 09 15:32:27 2001 +0100
+++ b/src/HOLCF/IOA/meta_theory/Seq.thy	Tue Jan 09 15:36:30 2001 +0100
@@ -36,7 +36,7 @@
    "Finite"     :: "'a seq => bool"
 
 translations
-   "xs @@ ys" == "sconc`xs`ys"
+   "xs @@ ys" == "sconc$xs$ys"
    "Finite x" == "x:sfinite"
    "~(Finite x)" =="x~:sfinite"
 
@@ -47,63 +47,63 @@
 (* f not possible at lhs, as "pattern matching" only for % x arguments,
    f cannot be written at rhs in front, as fix_eq3 does not apply later *)
 smap_def
-  "smap == (fix`(LAM h f tr. case tr of 
+  "smap == (fix$(LAM h f tr. case tr of 
       nil   => nil
-    | x##xs => f`x ## h`f`xs))"
+    | x##xs => f$x ## h$f$xs))"
 
 sfilter_def       
-  "sfilter == (fix`(LAM h P t. case t of 
+  "sfilter == (fix$(LAM h P t. case t of 
 	   nil => nil
-	 | x##xs => If P`x                                 
-                    then x##(h`P`xs)
-                    else     h`P`xs
+	 | x##xs => If P$x                                 
+                    then x##(h$P$xs)
+                    else     h$P$xs
                     fi))" 
 sforall_def
-  "sforall P t == (sforall2`P`t ~=FF)" 
+  "sforall P t == (sforall2$P$t ~=FF)" 
 
 
 sforall2_def
-  "sforall2 == (fix`(LAM h P t. case t of 
+  "sforall2 == (fix$(LAM h P t. case t of 
 	   nil => TT
-	 | x##xs => P`x andalso h`P`xs))"
+	 | x##xs => P$x andalso h$P$xs))"
   
 sconc_def
-  "sconc == (fix`(LAM h t1 t2. case t1 of 
+  "sconc == (fix$(LAM h t1 t2. case t1 of 
                nil       => t2
-             | x##xs => x##(h`xs`t2)))"
+             | x##xs => x##(h$xs$t2)))"
 
 slast_def
-  "slast == (fix`(LAM h t. case t of 
+  "slast == (fix$(LAM h t. case t of 
 	   nil => UU
-	 | x##xs => (If is_nil`xs                              
+	 | x##xs => (If is_nil$xs                              
                           then x
-                         else h`xs fi)))"
+                         else h$xs fi)))"
 
 stakewhile_def      
-  "stakewhile == (fix`(LAM h P t. case t of 
+  "stakewhile == (fix$(LAM h P t. case t of 
 	   nil => nil
-	 | x##xs => If P`x                                 
-                    then x##(h`P`xs)
+	 | x##xs => If P$x                                 
+                    then x##(h$P$xs)
                     else nil
                     fi))" 
 sdropwhile_def
-  "sdropwhile == (fix`(LAM h P t. case t of 
+  "sdropwhile == (fix$(LAM h P t. case t of 
 	   nil => nil
-	 | x##xs => If P`x                                 
-                    then h`P`xs
+	 | x##xs => If P$x                                 
+                    then h$P$xs
                     else t
                     fi))" 
 sflat_def
-  "sflat == (fix`(LAM h t. case t of 
+  "sflat == (fix$(LAM h t. case t of 
 	   nil => nil
-	 | x##xs => x @@ (h`xs)))"
+	 | x##xs => x @@ (h$xs)))"
 
 szip_def
-  "szip == (fix`(LAM h t1 t2. case t1 of 
+  "szip == (fix$(LAM h t1 t2. case t1 of 
                nil   => nil
              | x##xs => (case t2 of 
                           nil => UU 
-                        | y##ys => <x,y>##(h`xs`ys))))"
+                        | y##ys => <x,y>##(h$xs$ys))))"
 
 Partial_def
   "Partial x  == (seq_finite x) & ~(Finite x)"
diff -r a7897aebbffc -r f4745d77e620 src/HOLCF/IOA/meta_theory/Sequence.ML
--- a/src/HOLCF/IOA/meta_theory/Sequence.ML	Tue Jan 09 15:32:27 2001 +0100
+++ b/src/HOLCF/IOA/meta_theory/Sequence.ML	Tue Jan 09 15:36:30 2001 +0100
@@ -18,15 +18,15 @@
 (*                               Map                                *)
 (* ---------------------------------------------------------------- *)
 
-Goal "Map f`UU =UU";
+Goal "Map f$UU =UU";
 by (simp_tac (simpset() addsimps [Map_def]) 1);
 qed"Map_UU";
 
-Goal "Map f`nil =nil";
+Goal "Map f$nil =nil";
 by (simp_tac (simpset() addsimps [Map_def]) 1);
 qed"Map_nil";
 
-Goal "Map f`(x>>xs)=(f x) >> Map f`xs";
+Goal "Map f$(x>>xs)=(f x) >> Map f$xs";
 by (simp_tac (simpset() addsimps [Map_def, Consq_def,flift2_def]) 1);
 qed"Map_cons";
 
@@ -34,15 +34,15 @@
 (*                               Filter                             *)
 (* ---------------------------------------------------------------- *)
 
-Goal "Filter P`UU =UU";
+Goal "Filter P$UU =UU";
 by (simp_tac (simpset() addsimps [Filter_def]) 1);
 qed"Filter_UU";
 
-Goal "Filter P`nil =nil";
+Goal "Filter P$nil =nil";
 by (simp_tac (simpset() addsimps [Filter_def]) 1);
 qed"Filter_nil";
 
-Goal "Filter P`(x>>xs)= (if P x then x>>(Filter P`xs) else Filter P`xs)"; 
+Goal "Filter P$(x>>xs)= (if P x then x>>(Filter P$xs) else Filter P$xs)"; 
 by (simp_tac (simpset() addsimps [Filter_def, Consq_def,flift2_def,If_and_if]) 1);
 qed"Filter_cons";
 
@@ -76,15 +76,15 @@
 (*                               Takewhile                          *)
 (* ---------------------------------------------------------------- *)
 
-Goal "Takewhile P`UU =UU";
+Goal "Takewhile P$UU =UU";
 by (simp_tac (simpset() addsimps [Takewhile_def]) 1);
 qed"Takewhile_UU";
 
-Goal "Takewhile P`nil =nil";
+Goal "Takewhile P$nil =nil";
 by (simp_tac (simpset() addsimps [Takewhile_def]) 1);
 qed"Takewhile_nil";
 
-Goal "Takewhile P`(x>>xs)= (if P x then x>>(Takewhile P`xs) else nil)"; 
+Goal "Takewhile P$(x>>xs)= (if P x then x>>(Takewhile P$xs) else nil)"; 
 by (simp_tac (simpset() addsimps [Takewhile_def, Consq_def,flift2_def,If_and_if]) 1);
 qed"Takewhile_cons";
 
@@ -92,15 +92,15 @@
 (*                               Dropwhile                          *)
 (* ---------------------------------------------------------------- *)
 
-Goal "Dropwhile P`UU =UU";
+Goal "Dropwhile P$UU =UU";
 by (simp_tac (simpset() addsimps [Dropwhile_def]) 1);
 qed"Dropwhile_UU";
 
-Goal "Dropwhile P`nil =nil";
+Goal "Dropwhile P$nil =nil";
 by (simp_tac (simpset() addsimps [Dropwhile_def]) 1);
 qed"Dropwhile_nil";
 
-Goal "Dropwhile P`(x>>xs)= (if P x then Dropwhile P`xs else x>>xs)"; 
+Goal "Dropwhile P$(x>>xs)= (if P x then Dropwhile P$xs else x>>xs)"; 
 by (simp_tac (simpset() addsimps [Dropwhile_def, Consq_def,flift2_def,If_and_if]) 1);
 qed"Dropwhile_cons";
 
@@ -109,15 +109,15 @@
 (* ---------------------------------------------------------------- *)
 
 
-Goal "Last`UU =UU";
+Goal "Last$UU =UU";
 by (simp_tac (simpset() addsimps [Last_def]) 1);
 qed"Last_UU";
 
-Goal "Last`nil =UU";
+Goal "Last$nil =UU";
 by (simp_tac (simpset() addsimps [Last_def]) 1);
 qed"Last_nil";
 
-Goal "Last`(x>>xs)= (if xs=nil then Def x else Last`xs)"; 
+Goal "Last$(x>>xs)= (if xs=nil then Def x else Last$xs)"; 
 by (simp_tac (simpset() addsimps [Last_def, Consq_def]) 1);
 by (res_inst_tac [("x","xs")] seq.casedist 1);
 by (Asm_simp_tac 1);
@@ -129,15 +129,15 @@
 (*                               Flat                               *)
 (* ---------------------------------------------------------------- *)
 
-Goal "Flat`UU =UU";
+Goal "Flat$UU =UU";
 by (simp_tac (simpset() addsimps [Flat_def]) 1);
 qed"Flat_UU";
 
-Goal "Flat`nil =nil";
+Goal "Flat$nil =nil";
 by (simp_tac (simpset() addsimps [Flat_def]) 1);
 qed"Flat_nil";
 
-Goal "Flat`(x##xs)= x @@ (Flat`xs)"; 
+Goal "Flat$(x##xs)= x @@ (Flat$xs)"; 
 by (simp_tac (simpset() addsimps [Flat_def, Consq_def]) 1);
 qed"Flat_cons";
 
@@ -154,7 +154,7 @@
 \                                      Undef  => UU \
 \                                    | Def a => (case y of \
 \                                                  Undef => UU \
-\                                                | Def b => Def (a,b)##(Zip`xs`ys)))))";
+\                                                | Def b => Def (a,b)##(Zip$xs$ys)))))";
 by (rtac trans 1);
 by (rtac fix_eq2 1);
 by (rtac Zip_def 1);
@@ -162,29 +162,29 @@
 by (Simp_tac 1);
 qed"Zip_unfold";
 
-Goal "Zip`UU`y =UU";
+Goal "Zip$UU$y =UU";
 by (stac Zip_unfold 1);
 by (Simp_tac 1);
 qed"Zip_UU1";
 
-Goal "x~=nil ==> Zip`x`UU =UU";
+Goal "x~=nil ==> Zip$x$UU =UU";
 by (stac Zip_unfold 1);
 by (Simp_tac 1);
 by (res_inst_tac [("x","x")] seq.casedist 1);
 by (REPEAT (Asm_full_simp_tac 1));
 qed"Zip_UU2";
 
-Goal "Zip`nil`y =nil";
+Goal "Zip$nil$y =nil";
 by (stac Zip_unfold 1);
 by (Simp_tac 1);
 qed"Zip_nil";
 
-Goal "Zip`(x>>xs)`nil= UU"; 
+Goal "Zip$(x>>xs)$nil= UU"; 
 by (stac Zip_unfold 1);
 by (simp_tac (simpset() addsimps [Consq_def]) 1);
 qed"Zip_cons_nil";
 
-Goal "Zip`(x>>xs)`(y>>ys)= (x,y) >> Zip`xs`ys"; 
+Goal "Zip$(x>>xs)$(y>>ys)= (x,y) >> Zip$xs$ys"; 
 by (rtac trans 1);
 by (stac Zip_unfold 1);
 by (Simp_tac 1);
@@ -298,7 +298,7 @@
 by (etac monofun_cfun_arg 1);
 qed"Cons_inject_less_eq";
 
-Goal "seq_take (Suc n)`(a>>x) = a>> (seq_take n`x)";
+Goal "seq_take (Suc n)$(a>>x) = a>> (seq_take n$x)";
 by (simp_tac (simpset() addsimps [Consq_def]) 1);
 qed"seq_take_Cons";
 
@@ -365,11 +365,11 @@
 
 section "HD,TL";
 
-Goal "HD`(x>>y) = Def x";
+Goal "HD$(x>>y) = Def x";
 by (simp_tac (simpset() addsimps [Consq_def]) 1);
 qed"HD_Cons";
 
-Goal "TL`(x>>y) = y";
+Goal "TL$(x>>y) = y";
 by (simp_tac (simpset() addsimps [Consq_def]) 1);
 qed"TL_Cons";
 
@@ -415,11 +415,11 @@
 Addsimps [FiniteConc];
 
 
-Goal "Finite s ==> Finite (Map f`s)";
+Goal "Finite s ==> Finite (Map f$s)";
 by (Seq_Finite_induct_tac 1);
 qed"FiniteMap1";
 
-Goal "Finite s ==> ! t. (s = Map f`t) --> Finite t";
+Goal "Finite s ==> ! t. (s = Map f$t) --> Finite t";
 by (Seq_Finite_induct_tac 1);
 by (strip_tac 1);
 by (Seq_case_simp_tac "t" 1);
@@ -430,7 +430,7 @@
 by (Asm_full_simp_tac 1);
 qed"FiniteMap2";
 
-Goal "Finite (Map f`s) = Finite s";
+Goal "Finite (Map f$s) = Finite s";
 by Auto_tac;
 by (etac (FiniteMap2 RS spec RS mp) 1);
 by (rtac refl 1);
@@ -438,7 +438,7 @@
 qed"Map2Finite";
 
 
-Goal "Finite s ==> Finite (Filter P`s)";
+Goal "Finite s ==> Finite (Filter P$s)";
 by (Seq_Finite_induct_tac 1);
 qed"FiniteFilter";
 
@@ -519,11 +519,11 @@
 
 section "Last";
 
-Goal "Finite s ==> s~=nil --> Last`s~=UU";
+Goal "Finite s ==> s~=nil --> Last$s~=UU";
 by (Seq_Finite_induct_tac  1);
 qed"Finite_Last1";
 
-Goal "Finite s ==> Last`s=UU --> s=nil";
+Goal "Finite s ==> Last$s=UU --> s=nil";
 by (Seq_Finite_induct_tac  1);
 by (fast_tac HOL_cs 1);
 qed"Finite_Last2";
@@ -535,11 +535,11 @@
 section "Filter, Conc";
 
 
-Goal "Filter P`(Filter Q`s) = Filter (%x. P x & Q x)`s";
+Goal "Filter P$(Filter Q$s) = Filter (%x. P x & Q x)$s";
 by (Seq_induct_tac "s" [Filter_def] 1);
 qed"FilterPQ";
 
-Goal "Filter P`(x @@ y) = (Filter P`x @@ Filter P`y)";
+Goal "Filter P$(x @@ y) = (Filter P$x @@ Filter P$y)";
 by (simp_tac (simpset() addsimps [Filter_def,sfiltersconc]) 1);
 qed"FilterConc";
 
@@ -547,24 +547,24 @@
 
 section "Map";
 
-Goal "Map f`(Map g`s) = Map (f o g)`s";
+Goal "Map f$(Map g$s) = Map (f o g)$s";
 by (Seq_induct_tac "s" [] 1);
 qed"MapMap";
 
-Goal "Map f`(x@@y) = (Map f`x) @@ (Map f`y)";
+Goal "Map f$(x@@y) = (Map f$x) @@ (Map f$y)";
 by (Seq_induct_tac "x" [] 1);
 qed"MapConc";
 
-Goal "Filter P`(Map f`x) = Map f`(Filter (P o f)`x)";
+Goal "Filter P$(Map f$x) = Map f$(Filter (P o f)$x)";
 by (Seq_induct_tac "x" [] 1);
 qed"MapFilter";
 
-Goal "nil = (Map f`s) --> s= nil";
+Goal "nil = (Map f$s) --> s= nil";
 by (Seq_case_simp_tac "s" 1);
 qed"nilMap";
 
 
-Goal "Forall P (Map f`s) = Forall (P o f) s";
+Goal "Forall P (Map f$s) = Forall (P o f) s";
 by (Seq_induct_tac "s" [Forall_def,sforall_def] 1);
 qed"ForallMap";
 
@@ -593,13 +593,13 @@
 
 Addsimps [Forall_Conc];
 
-Goal "Forall P s  --> Forall P (TL`s)";
+Goal "Forall P s  --> Forall P (TL$s)";
 by (Seq_induct_tac "s" [Forall_def,sforall_def] 1);
 qed"ForallTL1";
 
 bind_thm ("ForallTL",ForallTL1 RS mp);
 
-Goal "Forall P s  --> Forall P (Dropwhile Q`s)";
+Goal "Forall P s  --> Forall P (Dropwhile Q$s)";
 by (Seq_induct_tac "s" [Forall_def,sforall_def] 1);
 qed"ForallDropwhile1";
 
@@ -624,7 +624,7 @@
 qed"Forall_postfixclosed";
 
 
-Goal "((! x. P x --> (Q x = R x)) & Forall P tr) --> Filter Q`tr = Filter R`tr";
+Goal "((! x. P x --> (Q x = R x)) & Forall P tr) --> Filter Q$tr = Filter R$tr";
 by (Seq_induct_tac "tr" [Forall_def,sforall_def] 1);
 qed"ForallPFilterQR1";
 
@@ -636,12 +636,12 @@
 section "Forall, Filter";
 
 
-Goal "Forall P (Filter P`x)";
+Goal "Forall P (Filter P$x)";
 by (simp_tac (simpset() addsimps [Filter_def,Forall_def,forallPsfilterP]) 1);
 qed"ForallPFilterP";
 
 (* holds also in other direction, then equal to forallPfilterP *)
-Goal "Forall P x --> Filter P`x = x";
+Goal "Forall P x --> Filter P$x = x";
 by (Seq_induct_tac "x" [Forall_def,sforall_def,Filter_def] 1);
 qed"ForallPFilterPid1";
 
@@ -650,7 +650,7 @@
 
 (* holds also in other direction *)
 Goal "!! ys . Finite ys ==> \
-\   Forall (%x. ~P x) ys --> Filter P`ys = nil ";
+\   Forall (%x. ~P x) ys --> Filter P$ys = nil ";
 by (Seq_Finite_induct_tac 1);
 qed"ForallnPFilterPnil1";
 
@@ -659,7 +659,7 @@
 
 (* holds also in other direction *)
 Goal   "~Finite ys & Forall (%x. ~P x) ys \
-\                  --> Filter P`ys = UU ";
+\                  --> Filter P$ys = UU ";
 by (Seq_induct_tac "ys" [Forall_def,sforall_def] 1);
 qed"ForallnPFilterPUU1";
 
@@ -668,7 +668,7 @@
 
 (* inverse of ForallnPFilterPnil *)
 
-Goal "!! ys . Filter P`ys = nil --> \
+Goal "!! ys . Filter P$ys = nil --> \
 \   (Forall (%x. ~P x) ys & Finite ys)";
 by (res_inst_tac[("x","ys")] Seq_induct 1);
 (* adm *)
@@ -685,15 +685,15 @@
 
 (* inverse of ForallnPFilterPUU. proved by 2 lemmas because of adm problems *)
 
-Goal "Finite ys ==> Filter P`ys ~= UU";
+Goal "Finite ys ==> Filter P$ys ~= UU";
 by (Seq_Finite_induct_tac 1);
 qed"FilterUU_nFinite_lemma1";
 
-Goal "~ Forall (%x. ~P x) ys --> Filter P`ys ~= UU";
+Goal "~ Forall (%x. ~P x) ys --> Filter P$ys ~= UU";
 by (Seq_induct_tac "ys" [Forall_def,sforall_def] 1);
 qed"FilterUU_nFinite_lemma2";
 
-Goal   "Filter P`ys = UU ==> \
+Goal   "Filter P$ys = UU ==> \
 \                (Forall (%x. ~P x) ys  & ~Finite ys)";
 by (rtac conjI 1);
 by (cut_inst_tac [] (FilterUU_nFinite_lemma2 RS mp COMP rev_contrapos) 1);
@@ -703,14 +703,14 @@
 
 
 Goal  "!! Q P.[| Forall Q ys; Finite ys; !!x. Q x ==> ~P x|] \
-\   ==> Filter P`ys = nil";
+\   ==> Filter P$ys = nil";
 by (etac ForallnPFilterPnil 1);
 by (etac ForallPForallQ 1);
 by Auto_tac;
 qed"ForallQFilterPnil";
 
 Goal "!! Q P. [| ~Finite ys; Forall Q ys;  !!x. Q x ==> ~P x|] \
-\   ==> Filter P`ys = UU ";
+\   ==> Filter P$ys = UU ";
 by (etac ForallnPFilterPUU 1);
 by (etac ForallPForallQ 1);
 by Auto_tac;
@@ -723,20 +723,20 @@
 section "Takewhile, Forall, Filter";
 
 
-Goal "Forall P (Takewhile P`x)";
+Goal "Forall P (Takewhile P$x)";
 by (simp_tac (simpset() addsimps [Forall_def,Takewhile_def,sforallPstakewhileP]) 1);
 qed"ForallPTakewhileP";
 
 
-Goal"!! P. [| !!x. Q x==> P x |] ==> Forall P (Takewhile Q`x)";
+Goal"!! P. [| !!x. Q x==> P x |] ==> Forall P (Takewhile Q$x)";
 by (rtac ForallPForallQ 1);
 by (rtac ForallPTakewhileP 1);
 by Auto_tac;
 qed"ForallPTakewhileQ";
 
 
-Goal  "!! Q P.[| Finite (Takewhile Q`ys); !!x. Q x ==> ~P x |] \
-\   ==> Filter P`(Takewhile Q`ys) = nil";
+Goal  "!! Q P.[| Finite (Takewhile Q$ys); !!x. Q x ==> ~P x |] \
+\   ==> Filter P$(Takewhile Q$ys) = nil";
 by (etac ForallnPFilterPnil 1);
 by (rtac ForallPForallQ 1);
 by (rtac ForallPTakewhileP 1);
@@ -744,7 +744,7 @@
 qed"FilterPTakewhileQnil";
 
 Goal "!! Q P. [| !!x. Q x ==> P x |] ==> \
-\            Filter P`(Takewhile Q`ys) = (Takewhile Q`ys)";
+\            Filter P$(Takewhile Q$ys) = (Takewhile Q$ys)";
 by (rtac ForallPFilterPid 1);
 by (rtac ForallPForallQ 1);
 by (rtac ForallPTakewhileP 1);
@@ -754,28 +754,28 @@
 Addsimps [ForallPTakewhileP,ForallPTakewhileQ,
           FilterPTakewhileQnil,FilterPTakewhileQid];
 
-Goal "Takewhile P`(Takewhile P`s) = Takewhile P`s";
+Goal "Takewhile P$(Takewhile P$s) = Takewhile P$s";
 by (Seq_induct_tac "s" [Forall_def,sforall_def] 1);
 qed"Takewhile_idempotent";
 
-Goal "Forall P s --> Takewhile (%x. Q x | (~P x))`s = Takewhile Q`s";
+Goal "Forall P s --> Takewhile (%x. Q x | (~P x))$s = Takewhile Q$s";
 by (Seq_induct_tac "s" [Forall_def,sforall_def] 1);
 qed"ForallPTakewhileQnP";
 
-Goal "Forall P s --> Dropwhile (%x. Q x | (~P x))`s = Dropwhile Q`s";
+Goal "Forall P s --> Dropwhile (%x. Q x | (~P x))$s = Dropwhile Q$s";
 by (Seq_induct_tac "s" [Forall_def,sforall_def] 1);
 qed"ForallPDropwhileQnP";
 
 Addsimps [ForallPTakewhileQnP RS mp, ForallPDropwhileQnP RS mp];
 
 
-Goal "Forall P s --> Takewhile P`(s @@ t) = s @@ (Takewhile P`t)";
+Goal "Forall P s --> Takewhile P$(s @@ t) = s @@ (Takewhile P$t)";
 by (Seq_induct_tac "s" [Forall_def,sforall_def] 1);
 qed"TakewhileConc1";
 
 bind_thm("TakewhileConc",TakewhileConc1 RS mp);
 
-Goal "Finite s ==> Forall P s --> Dropwhile P`(s @@ t) = Dropwhile P`t";
+Goal "Finite s ==> Forall P s --> Dropwhile P$(s @@ t) = Dropwhile P$t";
 by (Seq_Finite_induct_tac 1);
 qed"DropwhileConc1";
 
@@ -788,9 +788,9 @@
 section "coinductive characterizations of Filter";
 
 
-Goal "HD`(Filter P`y) = Def x \
-\         --> y = ((Takewhile (%x. ~P x)`y) @@ (x >> TL`(Dropwhile (%a.~P a)`y)))  \
-\             & Finite (Takewhile (%x. ~ P x)`y)  & P x";
+Goal "HD$(Filter P$y) = Def x \
+\         --> y = ((Takewhile (%x. ~P x)$y) @@ (x >> TL$(Dropwhile (%a.~P a)$y)))  \
+\             & Finite (Takewhile (%x. ~ P x)$y)  & P x";
 
 (* FIX: pay attention: is only admissible with chain-finite package to be added to 
         adm test and Finite f x admissibility *)
@@ -804,16 +804,16 @@
 by (Asm_full_simp_tac 1); 
 qed"divide_Seq_lemma";
 
-Goal "(x>>xs) << Filter P`y  \
-\   ==> y = ((Takewhile (%a. ~ P a)`y) @@ (x >> TL`(Dropwhile (%a.~P a)`y))) \
-\      & Finite (Takewhile (%a. ~ P a)`y)  & P x";
+Goal "(x>>xs) << Filter P$y  \
+\   ==> y = ((Takewhile (%a. ~ P a)$y) @@ (x >> TL$(Dropwhile (%a.~P a)$y))) \
+\      & Finite (Takewhile (%a. ~ P a)$y)  & P x";
 by (rtac (divide_Seq_lemma RS mp) 1);
 by (dres_inst_tac [("fo","HD"),("xa","x>>xs")]  monofun_cfun_arg 1);
 by (Asm_full_simp_tac 1); 
 qed"divide_Seq";
 
  
-Goal "~Forall P y --> (? x. HD`(Filter (%a. ~P a)`y) = Def x)";
+Goal "~Forall P y --> (? x. HD$(Filter (%a. ~P a)$y) = Def x)";
 (* Pay attention: is only admissible with chain-finite package to be added to 
         adm test *)
 by (Seq_induct_tac "y" [Forall_def,sforall_def] 1);
@@ -821,8 +821,8 @@
 
 
 Goal "~Forall P y  \
-\  ==> ? x. y= (Takewhile P`y @@ (x >> TL`(Dropwhile P`y))) & \
-\      Finite (Takewhile P`y) & (~ P x)";
+\  ==> ? x. y= (Takewhile P$y @@ (x >> TL$(Dropwhile P$y))) & \
+\      Finite (Takewhile P$y) & (~ P x)";
 by (dtac (nForall_HDFilter RS mp) 1);
 by (safe_tac set_cs);
 by (res_inst_tac [("x","x")] exI 1);
@@ -846,15 +846,15 @@
 
 section "take_lemma";
 
-Goal "(!n. seq_take n`x = seq_take n`x') = (x = x')";
+Goal "(!n. seq_take n$x = seq_take n$x') = (x = x')";
 by (rtac iffI 1);
 by (resolve_tac seq.take_lemmas 1);
 by Auto_tac;
 qed"seq_take_lemma";
 
 Goal 
-"  ! n. ((! k. k < n --> seq_take k`y1 = seq_take k`y2) \
-\   --> seq_take n`(x @@ (t>>y1)) =  seq_take n`(x @@ (t>>y2)))";
+"  ! n. ((! k. k < n --> seq_take k$y1 = seq_take k$y2) \
+\   --> seq_take n$(x @@ (t>>y1)) =  seq_take n$(x @@ (t>>y2)))";
 by (Seq_induct_tac "x" [] 1);
 by (strip_tac 1);
 by (case_tac "n" 1);
@@ -864,8 +864,8 @@
 qed"take_reduction1";
 
 
-Goal "!! n.[| x=y; s=t; !! k. k<n ==> seq_take k`y1 = seq_take k`y2|] \
-\ ==> seq_take n`(x @@ (s>>y1)) =  seq_take n`(y @@ (t>>y2))";
+Goal "!! n.[| x=y; s=t; !! k. k<n ==> seq_take k$y1 = seq_take k$y2|] \
+\ ==> seq_take n$(x @@ (s>>y1)) =  seq_take n$(y @@ (t>>y2))";
 
 by (auto_tac (claset() addSIs [take_reduction1 RS spec RS mp],simpset()));
 qed"take_reduction";
@@ -875,8 +875,8 @@
    ------------------------------------------------------------------ *)
 
 Goal 
-"  ! n. ((! k. k < n --> seq_take k`y1 << seq_take k`y2) \
-\   --> seq_take n`(x @@ (t>>y1)) <<  seq_take n`(x @@ (t>>y2)))";
+"  ! n. ((! k. k < n --> seq_take k$y1 << seq_take k$y2) \
+\   --> seq_take n$(x @@ (t>>y1)) <<  seq_take n$(x @@ (t>>y2)))";
 by (Seq_induct_tac "x" [] 1);
 by (strip_tac 1);
 by (case_tac "n" 1);
@@ -886,14 +886,14 @@
 qed"take_reduction_less1";
 
 
-Goal "!! n.[| x=y; s=t;!! k. k<n ==> seq_take k`y1 << seq_take k`y2|] \
-\ ==> seq_take n`(x @@ (s>>y1)) <<  seq_take n`(y @@ (t>>y2))";
+Goal "!! n.[| x=y; s=t;!! k. k<n ==> seq_take k$y1 << seq_take k$y2|] \
+\ ==> seq_take n$(x @@ (s>>y1)) <<  seq_take n$(y @@ (t>>y2))";
 by (auto_tac (claset() addSIs [take_reduction_less1 RS spec RS mp],simpset()));
 qed"take_reduction_less";
 
 
 val prems = goalw thy [seq.take_def]
-"(!! n. seq_take n`s1 << seq_take n`s2)  ==> s1<<s2";
+"(!! n. seq_take n$s1 << seq_take n$s2)  ==> s1<<s2";
 
 by (res_inst_tac [("t","s1")] (seq.reach RS subst)  1);
 by (res_inst_tac [("t","s2")] (seq.reach RS subst)  1);
@@ -910,7 +910,7 @@
 qed"take_lemma_less1";
 
 
-Goal "(!n. seq_take n`x << seq_take n`x') = (x << x')";
+Goal "(!n. seq_take n$x << seq_take n$x') = (x << x')";
 by (rtac iffI 1);
 by (rtac take_lemma_less1 1);
 by Auto_tac;
@@ -931,8 +931,8 @@
 
 Goal "!! Q. [|!! s. [| Forall Q s; A s |] ==> (f s) = (g s) ; \
 \           !! s1 s2 y. [| Forall Q s1; Finite s1; ~ Q y; A (s1 @@ y>>s2)|] \
-\                         ==> ! n. seq_take n`(f (s1 @@ y>>s2)) \
-\                                = seq_take n`(g (s1 @@ y>>s2)) |] \
+\                         ==> ! n. seq_take n$(f (s1 @@ y>>s2)) \
+\                                = seq_take n$(g (s1 @@ y>>s2)) |] \
 \              ==> A x --> (f x)=(g x)";
 by (case_tac "Forall Q x" 1);
 by (auto_tac (claset() addSDs [divide_Seq3],simpset()));
@@ -951,10 +951,10 @@
 
 Goal 
 "!! Q. [|!! s. [| Forall Q s; A s |] ==> (f s) = (g s) ; \
-\        !! s1 s2 y n. [| ! t. A t --> seq_take n`(f t) = seq_take n`(g t);\
+\        !! s1 s2 y n. [| ! t. A t --> seq_take n$(f t) = seq_take n$(g t);\
 \                         Forall Q s1; Finite s1; ~ Q y; A (s1 @@ y>>s2) |] \
-\                         ==>   seq_take (Suc n)`(f (s1 @@ y>>s2)) \
-\                             = seq_take (Suc n)`(g (s1 @@ y>>s2)) |] \
+\                         ==>   seq_take (Suc n)$(f (s1 @@ y>>s2)) \
+\                             = seq_take (Suc n)$(g (s1 @@ y>>s2)) |] \
 \              ==> A x --> (f x)=(g x)";
 by (rtac impI 1);
 by (resolve_tac seq.take_lemmas 1);
@@ -973,10 +973,10 @@
 
 Goal 
 "!! Q. [|!! s. [| Forall Q s; A s |] ==> (f s) = (g s) ; \
-\        !! s1 s2 y n. [| ! t m. m < n --> A t --> seq_take m`(f t) = seq_take m`(g t);\
+\        !! s1 s2 y n. [| ! t m. m < n --> A t --> seq_take m$(f t) = seq_take m$(g t);\
 \                         Forall Q s1; Finite s1; ~ Q y; A (s1 @@ y>>s2) |] \
-\                         ==>   seq_take n`(f (s1 @@ y>>s2)) \
-\                             = seq_take n`(g (s1 @@ y>>s2)) |] \
+\                         ==>   seq_take n$(f (s1 @@ y>>s2)) \
+\                             = seq_take n$(g (s1 @@ y>>s2)) |] \
 \              ==> A x --> (f x)=(g x)";
 by (rtac impI 1);
 by (resolve_tac seq.take_lemmas 1);
@@ -1025,10 +1025,10 @@
 
 Goal 
 "!! Q. [|!! s h1 h2. [| Forall Q s; A s h1 h2|] ==> (f s h1 h2) = (g s h1 h2) ; \
-\  !! s1 s2 y n. [| ! t h1 h2 m. m < n --> (A t h1 h2) --> seq_take m`(f t h1 h2) = seq_take m`(g t h1 h2);\
+\  !! s1 s2 y n. [| ! t h1 h2 m. m < n --> (A t h1 h2) --> seq_take m$(f t h1 h2) = seq_take m$(g t h1 h2);\
 \                         Forall Q s1; Finite s1; ~ Q y; A (s1 @@ y>>s2) h1 h2|] \
-\                         ==>   seq_take n`(f (s1 @@ y>>s2) h1 h2) \
-\                             = seq_take n`(g (s1 @@ y>>s2) h1 h2) |] \
+\                         ==>   seq_take n$(f (s1 @@ y>>s2) h1 h2) \
+\                             = seq_take n$(g (s1 @@ y>>s2) h1 h2) |] \
 \              ==> ! h1 h2. (A x h1 h2) --> (f x h1 h2)=(g x h1 h2)";
 by (strip_tac 1);
 by (resolve_tac seq.take_lemmas 1);
@@ -1049,14 +1049,14 @@
 
 Goal 
 "!! Q. [|!! s. Forall Q s ==> P ((f s) = (g s)) ; \
-\        !! s1 s2 y n. [| ! t m. m < n --> P (seq_take m`(f t) = seq_take m`(g t));\
+\        !! s1 s2 y n. [| ! t m. m < n --> P (seq_take m$(f t) = seq_take m$(g t));\
 \                         Forall Q s1; Finite s1; ~ Q y|] \
-\                         ==>   P (seq_take n`(f (s1 @@ y>>s2)) \
-\                                   = seq_take n`(g (s1 @@ y>>s2))) |] \
+\                         ==>   P (seq_take n$(f (s1 @@ y>>s2)) \
+\                                   = seq_take n$(g (s1 @@ y>>s2))) |] \
 \              ==> P ((f x)=(g x))";
 
 by (res_inst_tac [("t","f x = g x"),
-                  ("s","!n. seq_take n`(f x) = seq_take n`(g x)")] subst 1);
+                  ("s","!n. seq_take n$(f x) = seq_take n$(g x)")] subst 1);
 by (rtac seq_take_lemma 1);
 
 wie ziehe ich n durch P, d.h. evtl. ns in P muessen umbenannt werden.....
@@ -1079,10 +1079,10 @@
 Goal 
 "!! Q. [| A UU  ==> (f UU) = (g UU) ; \
 \         A nil ==> (f nil) = (g nil) ; \
-\         !! s y n. [| ! t. A t --> seq_take n`(f t) = seq_take n`(g t);\
+\         !! s y n. [| ! t. A t --> seq_take n$(f t) = seq_take n$(g t);\
 \                    A (y>>s) |]   \
-\                    ==>   seq_take (Suc n)`(f (y>>s)) \
-\                        = seq_take (Suc n)`(g (y>>s)) |] \
+\                    ==>   seq_take (Suc n)$(f (y>>s)) \
+\                        = seq_take (Suc n)$(g (y>>s)) |] \
 \              ==> A x --> (f x)=(g x)";
 by (rtac impI 1);
 by (resolve_tac seq.take_lemmas 1);
@@ -1111,26 +1111,26 @@
 (* In general: How to do this case without the same adm problems 
    as for the entire proof ? *) 
 Goal "Forall (%x.~(P x & Q x)) s \
-\         --> Filter P`(Filter Q`s) =\
-\             Filter (%x. P x & Q x)`s";
+\         --> Filter P$(Filter Q$s) =\
+\             Filter (%x. P x & Q x)$s";
 
 by (Seq_induct_tac "s" [Forall_def,sforall_def] 1);
 qed"Filter_lemma1";
 
 Goal "Finite s ==>  \
 \         (Forall (%x. (~P x) | (~ Q x)) s  \
-\         --> Filter P`(Filter Q`s) = nil)";
+\         --> Filter P$(Filter Q$s) = nil)";
 by (Seq_Finite_induct_tac 1);
 qed"Filter_lemma2";
 
 Goal "Finite s ==>  \
 \         Forall (%x. (~P x) | (~ Q x)) s  \
-\         --> Filter (%x. P x & Q x)`s = nil";
+\         --> Filter (%x. P x & Q x)$s = nil";
 by (Seq_Finite_induct_tac 1);
 qed"Filter_lemma3";
 
 
-Goal "Filter P`(Filter Q`s) = Filter (%x. P x & Q x)`s";
+Goal "Filter P$(Filter Q$s) = Filter (%x. P x & Q x)$s";
 by (res_inst_tac [("A1","%x. True") 
                  ,("Q1","%x.~(P x & Q x)"),("x1","s")]
                  (take_lemma_induct RS mp) 1);
@@ -1149,7 +1149,7 @@
 
 
 
-Goal "Map f`(x@@y) = (Map f`x) @@ (Map f`y)";
+Goal "Map f$(x@@y) = (Map f$x) @@ (Map f$y)";
 by (res_inst_tac [("A1","%x. True"), ("x1","x")]
     (take_lemma_in_eq_out RS mp) 1);
 by Auto_tac;
diff -r a7897aebbffc -r f4745d77e620 src/HOLCF/IOA/meta_theory/Sequence.thy
--- a/src/HOLCF/IOA/meta_theory/Sequence.thy	Tue Jan 09 15:32:27 2001 +0100
+++ b/src/HOLCF/IOA/meta_theory/Sequence.thy	Tue Jan 09 15:36:30 2001 +0100
@@ -42,7 +42,7 @@
 
 translations
 
-  "a>>s"         == "Consq a`s"
+  "a>>s"         == "Consq a$s"
   "[x, xs!]"     == "x>>[xs!]"
   "[x!]"         == "x>>nil"
   "[x, xs?]"     == "x>>[xs?]"
@@ -53,22 +53,22 @@
 
 Consq_def     "Consq a == LAM s. Def a ## s"
 
-Filter_def    "Filter P == sfilter`(flift2 P)"
+Filter_def    "Filter P == sfilter$(flift2 P)"
 
-Map_def       "Map f  == smap`(flift2 f)"
+Map_def       "Map f  == smap$(flift2 f)"
 
 Forall_def    "Forall P == sforall (flift2 P)"
 
 Last_def      "Last == slast"
 
-Dropwhile_def "Dropwhile P == sdropwhile`(flift2 P)"
+Dropwhile_def "Dropwhile P == sdropwhile$(flift2 P)"
 
-Takewhile_def "Takewhile P == stakewhile`(flift2 P)"
+Takewhile_def "Takewhile P == stakewhile$(flift2 P)"
 
 Flat_def      "Flat == sflat"
 
 Zip_def
-  "Zip == (fix`(LAM h t1 t2. case t1 of 
+  "Zip == (fix$(LAM h t1 t2. case t1 of 
                nil   => nil
              | x##xs => (case t2 of 
                           nil => UU 
@@ -76,13 +76,13 @@
                                       Undef  => UU
                                     | Def a => (case y of 
                                                   Undef => UU
-                                                | Def b => Def (a,b)##(h`xs`ys))))))"
+                                                | Def b => Def (a,b)##(h$xs$ys))))))"
 
-Filter2_def    "Filter2 P == (fix`(LAM h t. case t of 
+Filter2_def    "Filter2 P == (fix$(LAM h t. case t of 
             nil => nil
 	  | x##xs => (case x of Undef => UU | Def y => (if P y                                 
-                     then x##(h`xs)
-                     else     h`xs))))" 
+                     then x##(h$xs)
+                     else     h$xs))))" 
 
 rules
 
diff -r a7897aebbffc -r f4745d77e620 src/HOLCF/IOA/meta_theory/ShortExecutions.ML
--- a/src/HOLCF/IOA/meta_theory/ShortExecutions.ML	Tue Jan 09 15:32:27 2001 +0100
+++ b/src/HOLCF/IOA/meta_theory/ShortExecutions.ML	Tue Jan 09 15:36:30 2001 +0100
@@ -29,24 +29,24 @@
 \    | x##xs => \
 \      (case x of\ 
 \        Undef => UU\
-\      | Def y => (Takewhile (%a.~ P a)`s)\
-\                  @@ (y>>(oraclebuild P`(TL`(Dropwhile (%a.~ P a)`s))`xs))\
+\      | Def y => (Takewhile (%a.~ P a)$s)\
+\                  @@ (y>>(oraclebuild P$(TL$(Dropwhile (%a.~ P a)$s))$xs))\
 \      )\
 \    )");
 
-Goal "oraclebuild P`sch`UU = UU";
+Goal "oraclebuild P$sch$UU = UU";
 by (stac oraclebuild_unfold 1);
 by (Simp_tac 1);
 qed"oraclebuild_UU";
 
-Goal "oraclebuild P`sch`nil = nil";
+Goal "oraclebuild P$sch$nil = nil";
 by (stac oraclebuild_unfold 1);
 by (Simp_tac 1);
 qed"oraclebuild_nil";
 
-Goal "oraclebuild P`s`(x>>t) = \
-\         (Takewhile (%a.~ P a)`s)   \
-\          @@ (x>>(oraclebuild P`(TL`(Dropwhile (%a.~ P a)`s))`t))";     
+Goal "oraclebuild P$s$(x>>t) = \
+\         (Takewhile (%a.~ P a)$s)   \
+\          @@ (x>>(oraclebuild P$(TL$(Dropwhile (%a.~ P a)$s))$t))";     
 by (rtac trans 1);
 by (stac oraclebuild_unfold 1);
 by (asm_full_simp_tac (simpset() addsimps [Consq_def]) 1);
@@ -63,7 +63,7 @@
 Goalw [Cut_def]
 "[| Forall (%a.~ P a) s; Finite s|] \
 \           ==> Cut P s =nil";
-by (subgoal_tac "Filter P`s = nil" 1);
+by (subgoal_tac "Filter P$s = nil" 1);
 by (asm_simp_tac (simpset() addsimps [oraclebuild_nil]) 1);
 by (rtac ForallQFilterPnil 1);
 by (REPEAT (atac 1));
@@ -72,7 +72,7 @@
 Goalw [Cut_def]
 "[| Forall (%a.~ P a) s; ~Finite s|] \
 \           ==> Cut P s =UU";
-by (subgoal_tac "Filter P`s= UU" 1);
+by (subgoal_tac "Filter P$s= UU" 1);
 by (asm_simp_tac (simpset() addsimps [oraclebuild_UU]) 1);
 by (rtac ForallQFilterPUU 1);
 by (REPEAT (atac 1));
@@ -93,7 +93,7 @@
 (* ---------------------------------------------------------------- *)
 
 
-Goal "Filter P`s = Filter P`(Cut P s)";
+Goal "Filter P$s = Filter P$(Cut P s)";
 
 by (res_inst_tac [("A1","%x. True")
                  ,("Q1","%x.~ P x"), ("x1","s")]
@@ -128,7 +128,7 @@
 qed"Cut_idemp";
 
 
-Goal "Map f`(Cut (P o f) s) = Cut P (Map f`s)";
+Goal "Map f$(Cut (P o f) s) = Cut P (Map f$s)";
 
 by (res_inst_tac [("A1","%x. True")
                  ,("Q1","%x.~ P (f x)"), ("x1","s")]
@@ -200,13 +200,13 @@
 
 
 Goalw [schedules_def,has_schedule_def]
- "[|sch : schedules A ; tr = Filter (%a. a:ext A)`sch|] \
+ "[|sch : schedules A ; tr = Filter (%a. a:ext A)$sch|] \
 \   ==> ? sch. sch : schedules A & \
-\              tr = Filter (%a. a:ext A)`sch &\
+\              tr = Filter (%a. a:ext A)$sch &\
 \              LastActExtsch A sch";
 
 by (safe_tac set_cs);
-by (res_inst_tac [("x","filter_act`(Cut (%a. fst a:ext A) (snd ex))")] exI 1);
+by (res_inst_tac [("x","filter_act$(Cut (%a. fst a:ext A) (snd ex))")] exI 1);
 by (asm_full_simp_tac (simpset() addsimps [executions_def]) 1);
 by (pair_tac "ex" 1);
 by (safe_tac set_cs);
@@ -220,7 +220,7 @@
 (* Subgoal 2:  Lemma:  Filter P s = Filter P (Cut P s) *)
 
 by (simp_tac (simpset() addsimps [filter_act_def]) 1);
-by (subgoal_tac "Map fst`(Cut (%a. fst a: ext A) y)= Cut (%a. a:ext A) (Map fst`y)" 1);
+by (subgoal_tac "Map fst$(Cut (%a. fst a: ext A) y)= Cut (%a. a:ext A) (Map fst$y)" 1);
 
 by (rtac (rewrite_rule [o_def] MapCut) 2);
 by (asm_full_simp_tac (simpset() addsimps [FilterCut RS sym]) 1);
@@ -228,7 +228,7 @@
 (* Subgoal 3: Lemma: Cut idempotent  *)
 
 by (simp_tac (simpset() addsimps [LastActExtsch_def,filter_act_def]) 1);
-by (subgoal_tac "Map fst`(Cut (%a. fst a: ext A) y)= Cut (%a. a:ext A) (Map fst`y)" 1);
+by (subgoal_tac "Map fst$(Cut (%a. fst a: ext A) y)= Cut (%a. a:ext A) (Map fst$y)" 1);
 by (rtac (rewrite_rule [o_def] MapCut) 2);
 by (asm_full_simp_tac (simpset() addsimps [Cut_idemp]) 1);
 qed"exists_LastActExtsch";
@@ -239,7 +239,7 @@
 (* ---------------------------------------------------------------- *)
 
 Goalw [LastActExtsch_def]
-  "[| LastActExtsch A sch; Filter (%x. x:ext A)`sch = nil |] \
+  "[| LastActExtsch A sch; Filter (%x. x:ext A)$sch = nil |] \
 \   ==> sch=nil";
 by (dtac FilternPnilForallP 1);
 by (etac conjE 1);
@@ -249,7 +249,7 @@
 qed"LastActExtimplnil";
 
 Goalw [LastActExtsch_def]
-  "[| LastActExtsch A sch; Filter (%x. x:ext A)`sch = UU |] \
+  "[| LastActExtsch A sch; Filter (%x. x:ext A)$sch = UU |] \
 \   ==> sch=UU";
 by (dtac FilternPUUForallP 1);
 by (etac conjE 1);
diff -r a7897aebbffc -r f4745d77e620 src/HOLCF/IOA/meta_theory/ShortExecutions.thy
--- a/src/HOLCF/IOA/meta_theory/ShortExecutions.thy	Tue Jan 09 15:32:27 2001 +0100
+++ b/src/HOLCF/IOA/meta_theory/ShortExecutions.thy	Tue Jan 09 15:36:30 2001 +0100
@@ -28,19 +28,19 @@
   "LastActExtsch A sch == (Cut (%x. x: ext A) sch = sch)"
 
 (* LastActExtex_def
-  "LastActExtex A ex == LastActExtsch A (filter_act`ex)" *)
+  "LastActExtex A ex == LastActExtsch A (filter_act$ex)" *)
 
 Cut_def
-  "Cut P s == oraclebuild P`s`(Filter P`s)"
+  "Cut P s == oraclebuild P$s$(Filter P$s)"
 
 oraclebuild_def
-  "oraclebuild P == (fix`(LAM h s t. case t of 
+  "oraclebuild P == (fix$(LAM h s t. case t of 
        nil => nil
     | x##xs => 
       (case x of 
         Undef => UU
-      | Def y => (Takewhile (%x.~P x)`s)
-                  @@ (y>>(h`(TL`(Dropwhile (%x.~ P x)`s))`xs))
+      | Def y => (Takewhile (%x.~P x)$s)
+                  @@ (y>>(h$(TL$(Dropwhile (%x.~ P x)$s))$xs))
       )
     ))"
 
@@ -53,7 +53,7 @@
   "Finite s ==> (? y. s = Cut P s @@ y)"
 
 LastActExtsmall1
-  "LastActExtsch A sch ==> LastActExtsch A (TL`(Dropwhile P`sch))"
+  "LastActExtsch A sch ==> LastActExtsch A (TL$(Dropwhile P$sch))"
 
 LastActExtsmall2
   "[| Finite sch1; LastActExtsch A (sch1 @@ sch2) |] ==> LastActExtsch A sch2"
diff -r a7897aebbffc -r f4745d77e620 src/HOLCF/IOA/meta_theory/SimCorrectness.ML
--- a/src/HOLCF/IOA/meta_theory/SimCorrectness.ML	Tue Jan 09 15:32:27 2001 +0100
+++ b/src/HOLCF/IOA/meta_theory/SimCorrectness.ML	Tue Jan 09 15:36:30 2001 +0100
@@ -24,8 +24,8 @@
 \                                 T' = @t'. ? ex1. (t,t'):R & move A ex1 s a t' \
 \                             in \
 \                                (@cex. move A cex s a T')  \
-\                              @@ ((corresp_ex_simC A R `xs) T'))   \
-\                        `x) ))";
+\                              @@ ((corresp_ex_simC A R $xs) T'))   \
+\                        $x) ))";
 by (rtac trans 1);
 by (rtac fix_eq2 1);
 by (rtac corresp_ex_simC_def 1);
@@ -33,21 +33,21 @@
 by (simp_tac (simpset() addsimps [flift1_def]) 1);
 qed"corresp_ex_simC_unfold";
 
-Goal "(corresp_ex_simC A R`UU) s=UU";
+Goal "(corresp_ex_simC A R$UU) s=UU";
 by (stac corresp_ex_simC_unfold 1);
 by (Simp_tac 1);
 qed"corresp_ex_simC_UU";
 
-Goal "(corresp_ex_simC A R`nil) s = nil";
+Goal "(corresp_ex_simC A R$nil) s = nil";
 by (stac corresp_ex_simC_unfold 1);
 by (Simp_tac 1);
 qed"corresp_ex_simC_nil";
 
-Goal "(corresp_ex_simC A R`((a,t)>>xs)) s = \
+Goal "(corresp_ex_simC A R$((a,t)>>xs)) s = \
 \          (let T' = @t'. ? ex1. (t,t'):R & move A ex1 s a t' \
 \           in  \
 \            (@cex. move A cex s a T')  \ 
-\             @@ ((corresp_ex_simC A R`xs) T'))";
+\             @@ ((corresp_ex_simC A R$xs) T'))";
 by (rtac trans 1);
 by (stac corresp_ex_simC_unfold 1);
 by (asm_full_simp_tac (simpset() addsimps [Consq_def,flift1_def]) 1);
@@ -128,7 +128,7 @@
 Goal
    "[|is_simulation R C A; reachable C s; s-a--C-> t; (s,s'):R|] ==>\
 \   let T' = @t'. ? ex1. (t,t'):R & move A ex1 s' a t' in \
-\     mk_trace A`((@x. move A x s' a T')) = \
+\     mk_trace A$((@x. move A x s' a T')) = \
 \       (if a:ext A then a>>nil else nil)";
 by (cut_inst_tac [] move_is_move_sim 1);
 by (REPEAT (assume_tac 1));
@@ -160,7 +160,7 @@
 Goal 
   "[|is_simulation R C A; ext C = ext A|] ==>  \     
 \        !s s'. reachable C s & is_exec_frag C (s,ex) & (s,s'): R --> \
-\            mk_trace C`ex = mk_trace A`((corresp_ex_simC A R`ex) s')";
+\            mk_trace C$ex = mk_trace A$((corresp_ex_simC A R$ex) s')";
 
 by (pair_induct_tac "ex" [is_exec_frag_def] 1);
 (* cons case *) 
@@ -190,7 +190,7 @@
 Goal 
  "[| is_simulation R C A |] ==>\
 \ !s s'. reachable C s & is_exec_frag C (s,ex) & (s,s'):R  \
-\ --> is_exec_frag A (s',(corresp_ex_simC A R`ex) s')"; 
+\ --> is_exec_frag A (s',(corresp_ex_simC A R$ex) s')"; 
 
 by (Asm_full_simp_tac 1);
 by (pair_induct_tac "ex" [is_exec_frag_def] 1);
diff -r a7897aebbffc -r f4745d77e620 src/HOLCF/IOA/meta_theory/SimCorrectness.thy
--- a/src/HOLCF/IOA/meta_theory/SimCorrectness.thy	Tue Jan 09 15:32:27 2001 +0100
+++ b/src/HOLCF/IOA/meta_theory/SimCorrectness.thy	Tue Jan 09 15:36:30 2001 +0100
@@ -23,17 +23,17 @@
 corresp_ex_sim_def
   "corresp_ex_sim A R ex == let S'= (@s'.(fst ex,s'):R & s': starts_of A)
                             in 
-                               (S',(corresp_ex_simC A R`(snd ex)) S')"
+                               (S',(corresp_ex_simC A R$(snd ex)) S')"
 
 
 corresp_ex_simC_def
-  "corresp_ex_simC A R  == (fix`(LAM h ex. (%s. case ex of 
+  "corresp_ex_simC A R  == (fix$(LAM h ex. (%s. case ex of 
       nil =>  nil
     | x##xs => (flift1 (%pr. let a = (fst pr); t = (snd pr);
                                  T' = @t'. ? ex1. (t,t'):R & move A ex1 s a t' 
                              in
                                 (@cex. move A cex s a T')
-                                 @@ ((h`xs) T'))
-                        `x) )))"
+                                 @@ ((h$xs) T'))
+                        $x) )))"
  
 end
\ No newline at end of file
diff -r a7897aebbffc -r f4745d77e620 src/HOLCF/IOA/meta_theory/Simulations.ML
--- a/src/HOLCF/IOA/meta_theory/Simulations.ML	Tue Jan 09 15:32:27 2001 +0100
+++ b/src/HOLCF/IOA/meta_theory/Simulations.ML	Tue Jan 09 15:36:30 2001 +0100
@@ -19,7 +19,7 @@
 
 
 Goalw [Image_def]
-"(R```{x} Int S ~= {}) = (? y. (x,y):R & y:S)";
+"(R``{x} Int S ~= {}) = (? y. (x,y):R & y:S)";
 by (simp_tac (simpset() addsimps [Int_non_empty]) 1);
 qed"Sim_start_convert";
 
diff -r a7897aebbffc -r f4745d77e620 src/HOLCF/IOA/meta_theory/Simulations.thy
--- a/src/HOLCF/IOA/meta_theory/Simulations.thy	Tue Jan 09 15:32:27 2001 +0100
+++ b/src/HOLCF/IOA/meta_theory/Simulations.thy	Tue Jan 09 15:36:30 2001 +0100
@@ -23,7 +23,7 @@
 
 is_simulation_def
   "is_simulation R C A ==                          
-   (!s:starts_of C. R```{s} Int starts_of A ~= {}) &        
+   (!s:starts_of C. R``{s} Int starts_of A ~= {}) &        
    (!s s' t a. reachable C s &                      
                s -a--C-> t   &
                (s,s') : R              
@@ -31,7 +31,7 @@
 
 is_backward_simulation_def
   "is_backward_simulation R C A ==                          
-   (!s:starts_of C. R```{s} <= starts_of A) &        
+   (!s:starts_of C. R``{s} <= starts_of A) &        
    (!s t t' a. reachable C s &                      
                s -a--C-> t   &
                (t,t') : R              
diff -r a7897aebbffc -r f4745d77e620 src/HOLCF/IOA/meta_theory/TL.ML
--- a/src/HOLCF/IOA/meta_theory/TL.ML	Tue Jan 09 15:32:27 2001 +0100
+++ b/src/HOLCF/IOA/meta_theory/TL.ML	Tue Jan 09 15:36:30 2001 +0100
@@ -106,7 +106,7 @@
 
 
 Goalw [tsuffix_def,suffix_def]
-"s~=UU & s~=nil --> tsuffix s2 (TL`s) --> tsuffix s2 s";
+"s~=UU & s~=nil --> tsuffix s2 (TL$s) --> tsuffix s2 s";
 by Auto_tac;
 by (Seq_case_simp_tac "s" 1);
 by (res_inst_tac [("x","a>>s1")] exI 1);
diff -r a7897aebbffc -r f4745d77e620 src/HOLCF/IOA/meta_theory/TL.thy
--- a/src/HOLCF/IOA/meta_theory/TL.thy	Tue Jan 09 15:32:27 2001 +0100
+++ b/src/HOLCF/IOA/meta_theory/TL.thy	Tue Jan 09 15:36:30 2001 +0100
@@ -50,7 +50,7 @@
 
 (* this means that for nil and UU the effect is unpredictable *)
 Init_def
-  "Init P s ==  (P (unlift (HD`s)))" 
+  "Init P s ==  (P (unlift (HD$s)))" 
 
 suffix_def
   "suffix s2 s == ? s1. (Finite s1  & s = s1 @@ s2)" 
@@ -62,7 +62,7 @@
   "([] P) s == ! s2. tsuffix s2 s --> P s2"
 
 Next_def
-  "(Next P) s == if (TL`s=UU | TL`s=nil) then (P s) else P (TL`s)"
+  "(Next P) s == if (TL$s=UU | TL$s=nil) then (P s) else P (TL$s)"
 
 Diamond_def
   "<> P == .~ ([] (.~ P))"
diff -r a7897aebbffc -r f4745d77e620 src/HOLCF/IOA/meta_theory/TLS.ML
--- a/src/HOLCF/IOA/meta_theory/TLS.ML	Tue Jan 09 15:32:27 2001 +0100
+++ b/src/HOLCF/IOA/meta_theory/TLS.ML	Tue Jan 09 15:36:30 2001 +0100
@@ -20,8 +20,8 @@
 Goal "ex2seqC  = (LAM ex. (%s. case ex of \
 \      nil =>  (s,None,s)>>nil   \
 \    | x##xs => (flift1 (%pr. \
-\                (s,Some (fst pr), snd pr)>> (ex2seqC`xs) (snd pr))  \
-\                `x)  \
+\                (s,Some (fst pr), snd pr)>> (ex2seqC$xs) (snd pr))  \
+\                $x)  \
 \      ))";
 by (rtac trans 1);
 by (rtac fix_eq2 1);
@@ -30,18 +30,18 @@
 by (simp_tac (simpset() addsimps [flift1_def]) 1);
 qed"ex2seqC_unfold";
 
-Goal "(ex2seqC `UU) s=UU";
+Goal "(ex2seqC $UU) s=UU";
 by (stac ex2seqC_unfold 1);
 by (Simp_tac 1);
 qed"ex2seqC_UU";
 
-Goal "(ex2seqC `nil) s = (s,None,s)>>nil";
+Goal "(ex2seqC $nil) s = (s,None,s)>>nil";
 by (stac ex2seqC_unfold 1);
 by (Simp_tac 1);
 qed"ex2seqC_nil";
 
-Goal "(ex2seqC `((a,t)>>xs)) s = \
-\          (s,Some a,t)>> ((ex2seqC`xs) t)";
+Goal "(ex2seqC $((a,t)>>xs)) s = \
+\          (s,Some a,t)>> ((ex2seqC$xs) t)";
 by (rtac trans 1);
 by (stac ex2seqC_unfold 1);
 by (asm_full_simp_tac (simpset() addsimps [Consq_def,flift1_def]) 1);
diff -r a7897aebbffc -r f4745d77e620 src/HOLCF/IOA/meta_theory/TLS.thy
--- a/src/HOLCF/IOA/meta_theory/TLS.thy	Tue Jan 09 15:32:27 2001 +0100
+++ b/src/HOLCF/IOA/meta_theory/TLS.thy	Tue Jan 09 15:36:30 2001 +0100
@@ -60,14 +60,14 @@
   "xt2 P tr == P (fst (snd tr))"
 
 ex2seq_def
-  "ex2seq ex == ((ex2seqC `(mkfin (snd ex))) (fst ex))"
+  "ex2seq ex == ((ex2seqC $(mkfin (snd ex))) (fst ex))"
 
 ex2seqC_def
-  "ex2seqC == (fix`(LAM h ex. (%s. case ex of 
+  "ex2seqC == (fix$(LAM h ex. (%s. case ex of 
       nil =>  (s,None,s)>>nil
     | x##xs => (flift1 (%pr.
-                (s,Some (fst pr), snd pr)>> (h`xs) (snd pr)) 
-                `x)
+                (s,Some (fst pr), snd pr)>> (h$xs) (snd pr)) 
+                $x)
       )))"
 
 validTE_def
diff -r a7897aebbffc -r f4745d77e620 src/HOLCF/IOA/meta_theory/Traces.ML
--- a/src/HOLCF/IOA/meta_theory/Traces.ML	Tue Jan 09 15:32:27 2001 +0100
+++ b/src/HOLCF/IOA/meta_theory/Traces.ML	Tue Jan 09 15:36:30 2001 +0100
@@ -26,15 +26,15 @@
 (* ---------------------------------------------------------------- *)
 
 
-Goal  "filter_act`UU = UU";
+Goal  "filter_act$UU = UU";
 by (simp_tac (simpset() addsimps [filter_act_def]) 1);
 qed"filter_act_UU";
 
-Goal  "filter_act`nil = nil";
+Goal  "filter_act$nil = nil";
 by (simp_tac (simpset() addsimps [filter_act_def]) 1);
 qed"filter_act_nil";
 
-Goal "filter_act`(x>>xs) = (fst x) >> filter_act`xs";
+Goal "filter_act$(x>>xs) = (fst x) >> filter_act$xs";
 by (simp_tac (simpset() addsimps [filter_act_def]) 1);
 qed"filter_act_cons";
 
@@ -45,18 +45,18 @@
 (*                             mk_trace                             *)
 (* ---------------------------------------------------------------- *)
 
-Goal "mk_trace A`UU=UU";
+Goal "mk_trace A$UU=UU";
 by (simp_tac (simpset() addsimps [mk_trace_def]) 1);
 qed"mk_trace_UU";
 
-Goal "mk_trace A`nil=nil";
+Goal "mk_trace A$nil=nil";
 by (simp_tac (simpset() addsimps [mk_trace_def]) 1);
 qed"mk_trace_nil";
 
-Goal "mk_trace A`(at >> xs) =    \
+Goal "mk_trace A$(at >> xs) =    \
 \            (if ((fst at):ext A)    \       
-\                 then (fst at) >> (mk_trace A`xs) \   
-\                 else mk_trace A`xs)";
+\                 then (fst at) >> (mk_trace A$xs) \   
+\                 else mk_trace A$xs)";
 
 by (asm_full_simp_tac (simpset() addsimps [mk_trace_def]) 1);
 qed"mk_trace_cons";
@@ -71,8 +71,8 @@
 Goal "is_exec_fragC A = (LAM ex. (%s. case ex of \
 \      nil => TT \
 \    | x##xs => (flift1 \ 
-\            (%p. Def ((s,p):trans_of A) andalso (is_exec_fragC A`xs) (snd p)) \
-\             `x) \
+\            (%p. Def ((s,p):trans_of A) andalso (is_exec_fragC A$xs) (snd p)) \
+\             $x) \
 \   ))";
 by (rtac trans 1);
 by (rtac fix_eq2 1);
@@ -81,19 +81,19 @@
 by (simp_tac (simpset() addsimps [flift1_def]) 1);
 qed"is_exec_fragC_unfold";
 
-Goal "(is_exec_fragC A`UU) s=UU";
+Goal "(is_exec_fragC A$UU) s=UU";
 by (stac is_exec_fragC_unfold 1);
 by (Simp_tac 1);
 qed"is_exec_fragC_UU";
 
-Goal "(is_exec_fragC A`nil) s = TT";
+Goal "(is_exec_fragC A$nil) s = TT";
 by (stac is_exec_fragC_unfold 1);
 by (Simp_tac 1);
 qed"is_exec_fragC_nil";
 
-Goal "(is_exec_fragC A`(pr>>xs)) s = \
+Goal "(is_exec_fragC A$(pr>>xs)) s = \
 \                        (Def ((s,pr):trans_of A) \
-\                andalso (is_exec_fragC A`xs)(snd pr))";
+\                andalso (is_exec_fragC A$xs)(snd pr))";
 by (rtac trans 1);
 by (stac is_exec_fragC_unfold 1);
 by (asm_full_simp_tac (simpset() addsimps [Consq_def,flift1_def]) 1);
@@ -163,7 +163,7 @@
    take the detour of schedules *)
 
 Goalw  [executions_def,mk_trace_def,has_trace_def,schedules_def,has_schedule_def] 
-"has_trace A b = (? ex:executions A. b = mk_trace A`(snd ex))";
+"has_trace A b = (? ex:executions A. b = mk_trace A$(snd ex))";
 
 by (safe_tac set_cs);
 (* 1 *)
@@ -173,7 +173,7 @@
 by (Simp_tac 1);
 by (Asm_simp_tac 1);
 (* 2 *)
-by (res_inst_tac[("x","filter_act`(snd ex)")] bexI 1);
+by (res_inst_tac[("x","filter_act$(snd ex)")] bexI 1);
 by (stac beta_cfun 1);
 by (cont_tacR 1);
 by (Simp_tac 1);
@@ -195,7 +195,7 @@
 
 Goal 
   "!! A. is_trans_of A ==> \
-\ ! s. is_exec_frag A (s,xs) --> Forall (%a. a:act A) (filter_act`xs)";
+\ ! s. is_exec_frag A (s,xs) --> Forall (%a. a:act A) (filter_act$xs)";
 
 by (pair_induct_tac "xs" [is_exec_frag_def,Forall_def,sforall_def] 1);
 (* main case *)
@@ -206,7 +206,7 @@
 
 Goal 
   "!! A.[|  is_trans_of A; x:executions A |] ==> \
-\ Forall (%a. a:act A) (filter_act`(snd x))";
+\ Forall (%a. a:act A) (filter_act$(snd x))";
 
 by (asm_full_simp_tac (simpset() addsimps [executions_def]) 1);
 by (pair_tac "x" 1);
diff -r a7897aebbffc -r f4745d77e620 src/HOLCF/IOA/meta_theory/Traces.thy
--- a/src/HOLCF/IOA/meta_theory/Traces.thy	Tue Jan 09 15:32:27 2001 +0100
+++ b/src/HOLCF/IOA/meta_theory/Traces.thy	Tue Jan 09 15:36:30 2001 +0100
@@ -74,15 +74,15 @@
 
 
 is_exec_frag_def
-  "is_exec_frag A ex ==  ((is_exec_fragC A`(snd ex)) (fst ex) ~= FF)"
+  "is_exec_frag A ex ==  ((is_exec_fragC A$(snd ex)) (fst ex) ~= FF)"
 
 
 is_exec_fragC_def
-  "is_exec_fragC A ==(fix`(LAM h ex. (%s. case ex of 
+  "is_exec_fragC A ==(fix$(LAM h ex. (%s. case ex of 
       nil => TT
     | x##xs => (flift1 
-            (%p. Def ((s,p):trans_of A) andalso (h`xs) (snd p)) 
-             `x)
+            (%p. Def ((s,p):trans_of A) andalso (h$xs) (snd p)) 
+             $x)
    )))" 
 
 
@@ -100,7 +100,7 @@
 
 has_schedule_def
   "has_schedule ioa sch ==                                               
-     (? ex:executions ioa. sch = filter_act`(snd ex))"
+     (? ex:executions ioa. sch = filter_act$(snd ex))"
 
 schedules_def
   "schedules ioa == {sch. has_schedule ioa sch}"
@@ -110,7 +110,7 @@
 
 has_trace_def
   "has_trace ioa tr ==                                               
-     (? sch:schedules ioa. tr = Filter (%a. a:ext(ioa))`sch)"
+     (? sch:schedules ioa. tr = Filter (%a. a:ext(ioa))$sch)"
  
 traces_def
   "traces ioa == {tr. has_trace ioa tr}"
@@ -118,18 +118,18 @@
 
 mk_trace_def
   "mk_trace ioa == LAM tr. 
-     Filter (%a. a:ext(ioa))`(filter_act`tr)"
+     Filter (%a. a:ext(ioa))$(filter_act$tr)"
 
 
 (*  ------------------- Fair Traces ------------------------------ *)
 
 laststate_def
-  "laststate ex == case Last`(snd ex) of
+  "laststate ex == case Last$(snd ex) of
                       Undef  => fst ex
                     | Def at => snd at"
 
 inf_often_def
-  "inf_often P s == Infinite (Filter P`s)"
+  "inf_often P s == Infinite (Filter P$s)"
 
 (*  filtering P yields a finite or partial sequence *)
 fin_often_def
@@ -166,7 +166,7 @@
   "fairexecutions A == {ex. ex:executions A & fair_ex A ex}"
 
 fairtraces_def
-  "fairtraces A == {mk_trace A`(snd ex) | ex. ex:fairexecutions A}"
+  "fairtraces A == {mk_trace A$(snd ex) | ex. ex:fairexecutions A}"
 
 
 (*  ------------------- Implementation ------------------------------ *)
diff -r a7897aebbffc -r f4745d77e620 src/HOLCF/domain/theorems.ML
--- a/src/HOLCF/domain/theorems.ML	Tue Jan 09 15:32:27 2001 +0100
+++ b/src/HOLCF/domain/theorems.ML	Tue Jan 09 15:36:30 2001 +0100
@@ -451,7 +451,7 @@
                                   asm_simp_tac take_ss 1 ::
                                   map (fn arg =>
                                    case_UU_tac (prems@con_rews) 1 (
-                           nth_elem(rec_of arg,dnames)^"_take n`"^vname arg))
+                           nth_elem(rec_of arg,dnames)^"_take n$"^vname arg))
                                   (filter is_nonlazy_rec args) @ [
                                   resolve_tac prems 1] @
                                   map (K (atac 1))      (nonlazy args) @
diff -r a7897aebbffc -r f4745d77e620 src/HOLCF/ex/Dagstuhl.thy
--- a/src/HOLCF/ex/Dagstuhl.thy	Tue Jan 09 15:32:27 2001 +0100
+++ b/src/HOLCF/ex/Dagstuhl.thy	Tue Jan 09 15:36:30 2001 +0100
@@ -10,8 +10,8 @@
 
 defs
 
-YS_def    "YS  == fix`(LAM x. y && x)"
-YYS_def   "YYS == fix`(LAM z. y && y && z)"
+YS_def    "YS  == fix$(LAM x. y && x)"
+YYS_def   "YYS == fix$(LAM z. y && y && z)"
   
 end
 
diff -r a7897aebbffc -r f4745d77e620 src/HOLCF/ex/Dnat.ML
--- a/src/HOLCF/ex/Dnat.ML	Tue Jan 09 15:32:27 2001 +0100
+++ b/src/HOLCF/ex/Dnat.ML	Tue Jan 09 15:36:30 2001 +0100
@@ -13,23 +13,23 @@
 
 bind_thm ("iterator_def2", fix_prover2 Dnat.thy iterator_def 
 	"iterator = (LAM n f x. case n of dzero => x | \
-\                                     dsucc`m => f`(iterator`m`f`x))");
+\                                     dsucc$m => f$(iterator$m$f$x))");
 
 (* ------------------------------------------------------------------------- *)
 (* recursive  properties                                                     *)
 (* ------------------------------------------------------------------------- *)
 
-Goal "iterator`UU`f`x = UU";
+Goal "iterator$UU$f$x = UU";
 by (stac iterator_def2 1);
 by (simp_tac (HOLCF_ss addsimps dnat.rews) 1);
 qed "iterator1";
 
-Goal "iterator`dzero`f`x = x";
+Goal "iterator$dzero$f$x = x";
 by (stac iterator_def2 1);
 by (simp_tac (HOLCF_ss addsimps dnat.rews) 1);
 qed "iterator2";
 
-Goal "n~=UU ==> iterator`(dsucc`n)`f`x = f`(iterator`n`f`x)";
+Goal "n~=UU ==> iterator$(dsucc$n)$f$x = f$(iterator$n$f$x)";
 by (rtac trans 1);
 by (stac iterator_def2 1);
 by (asm_simp_tac (HOLCF_ss addsimps dnat.rews) 1);
diff -r a7897aebbffc -r f4745d77e620 src/HOLCF/ex/Dnat.thy
--- a/src/HOLCF/ex/Dnat.thy	Tue Jan 09 15:32:27 2001 +0100
+++ b/src/HOLCF/ex/Dnat.thy	Tue Jan 09 15:36:30 2001 +0100
@@ -13,7 +13,7 @@
 constdefs
 
 iterator :: "dnat -> ('a -> 'a) -> 'a -> 'a"
-            "iterator == fix`(LAM h n f x . case n of dzero   => x
-                                                    | dsucc`m => f`(h`m`f`x))"
+            "iterator == fix$(LAM h n f x . case n of dzero   => x
+                                                    | dsucc$m => f$(h$m$f$x))"
 
 end
diff -r a7897aebbffc -r f4745d77e620 src/HOLCF/ex/Fix2.ML
--- a/src/HOLCF/ex/Fix2.ML	Tue Jan 09 15:32:27 2001 +0100
+++ b/src/HOLCF/ex/Fix2.ML	Tue Jan 09 15:36:30 2001 +0100
@@ -14,7 +14,7 @@
 qed "lemma1";
 
 
-Goal "gix`F=lub(range(%i. iterate i F UU))";
+Goal "gix$F=lub(range(%i. iterate i F UU))";
 by (rtac (lemma1 RS subst) 1);
 by (rtac fix_def2 1);
 qed "lemma2";
diff -r a7897aebbffc -r f4745d77e620 src/HOLCF/ex/Fix2.thy
--- a/src/HOLCF/ex/Fix2.thy	Tue Jan 09 15:32:27 2001 +0100
+++ b/src/HOLCF/ex/Fix2.thy	Tue Jan 09 15:36:30 2001 +0100
@@ -16,7 +16,7 @@
 
 rules
 
-gix1_def "F`(gix`F) = gix`F"
-gix2_def "F`y=y ==> gix`F << y"
+gix1_def "F$(gix$F) = gix$F"
+gix2_def "F$y=y ==> gix$F << y"
 
 end
diff -r a7897aebbffc -r f4745d77e620 src/HOLCF/ex/Focus_ex.ML
--- a/src/HOLCF/ex/Focus_ex.ML	Tue Jan 09 15:32:27 2001 +0100
+++ b/src/HOLCF/ex/Focus_ex.ML	Tue Jan 09 15:36:30 2001 +0100
@@ -4,20 +4,20 @@
 
 val prems = goal Focus_ex.thy
 "is_g(g) = \ 
-\ (? f. is_f(f) &  (!x.(? z. <g`x,z> = f`<x,z> &  \
-\                  (! w y. <y,w> = f`<x,w>  --> z << w))))";
+\ (? f. is_f(f) &  (!x.(? z. <g$x,z> = f$<x,z> &  \
+\                  (! w y. <y,w> = f$<x,w>  --> z << w))))";
 by (simp_tac (HOL_ss addsimps [is_g,is_net_g]) 1);
 by (fast_tac HOL_cs 1);
 val lemma1 = result();
 
 val prems = goal Focus_ex.thy
-"(? f. is_f(f) &  (!x. (? z. <g`x,z> = f`<x,z> &  \
-\                 (!w y. <y,w> = f`<x,w>  --> z << w)))) \
+"(? f. is_f(f) &  (!x. (? z. <g$x,z> = f$<x,z> &  \
+\                 (!w y. <y,w> = f$<x,w>  --> z << w)))) \
 \ = \ 
 \ (? f. is_f(f) &  (!x. ? z.\
-\       g`x = cfst`(f`<x,z>) &  \
-\         z = csnd`(f`<x,z>) &  \
-\       (! w y.  <y,w> = f`<x,w> --> z << w)))";
+\       g$x = cfst$(f$<x,z>) &  \
+\         z = csnd$(f$<x,z>) &  \
+\       (! w y.  <y,w> = f$<x,w> --> z << w)))";
 by (rtac iffI 1);
 by (etac exE 1);
 by (res_inst_tac [("x","f")] exI 1);
@@ -63,7 +63,7 @@
 by (REPEAT (etac conjE 1));
 by (etac conjI 1);
 by (strip_tac 1);
-by (res_inst_tac [("x","fix`(LAM k. csnd`(f`<x,k>))")] exI 1);
+by (res_inst_tac [("x","fix$(LAM k. csnd$(f$<x,k>))")] exI 1);
 by (rtac conjI 1);
  by (asm_simp_tac HOLCF_ss 1);
  by (rtac trans 1);
@@ -94,16 +94,16 @@
 by (eres_inst_tac [("x","x")] allE 1);
 by (etac exE 1);
 by (REPEAT (etac conjE 1));
-by (subgoal_tac "fix`(LAM k. csnd`(f`<x, k>)) = z" 1);
+by (subgoal_tac "fix$(LAM k. csnd$(f$<x, k>)) = z" 1);
  by (asm_simp_tac HOLCF_ss 1);
-by (subgoal_tac "! w y. f`<x, w> = <y, w>  --> z << w" 1);
+by (subgoal_tac "! w y. f$<x, w> = <y, w>  --> z << w" 1);
 by (rtac sym 1);
 by (rtac fix_eqI 1);
 by (asm_simp_tac HOLCF_ss 1);
 by (rtac allI 1);
 by (simp_tac HOLCF_ss 1);
 by (strip_tac 1);
-by (subgoal_tac "f`<x, za> = <cfst`(f`<x,za>),za>" 1);
+by (subgoal_tac "f$<x, za> = <cfst$(f$<x,za>),za>" 1);
 by (fast_tac HOL_cs 1);
 by (rtac trans 1);
 by (rtac (surjective_pairing_Cprod2 RS sym) 1);
diff -r a7897aebbffc -r f4745d77e620 src/HOLCF/ex/Focus_ex.thy
--- a/src/HOLCF/ex/Focus_ex.thy	Tue Jan 09 15:32:27 2001 +0100
+++ b/src/HOLCF/ex/Focus_ex.thy	Tue Jan 09 15:36:30 2001 +0100
@@ -30,7 +30,7 @@
 	input  channel x:'b 
 	output channel y:'c 
 is network
-	<y,z> = f`<x,z>
+	<y,z> = f$<x,z>
 end network
 end g
 
@@ -47,7 +47,7 @@
 		'c stream * ('b,'c) tc stream) => bool
 
 is_f f  = !i1 i2 o1 o2. 
-	f`<i1,i2> = <o1,o2> --> Rf(i1,i2,o1,o2)
+	f$<i1,i2> = <o1,o2> --> Rf(i1,i2,o1,o2)
 
 Specification of agent g is translated to predicate is_g which uses
 predicate is_net_g
@@ -56,13 +56,13 @@
 	    'b stream => 'c stream => bool
 
 is_net_g f x y = 
-	? z. <y,z> = f`<x,z> & 
-	!oy hz. <oy,hz> = f`<x,hz> --> z << hz 
+	? z. <y,z> = f$<x,z> & 
+	!oy hz. <oy,hz> = f$<x,hz> --> z << hz 
 
 
 is_g :: ('b stream -> 'c stream) => bool
 
-is_g g  = ? f. is_f f  & (!x y. g`x = y --> is_net_g f x y
+is_g g  = ? f. is_f f  & (!x y. g$x = y --> is_net_g f x y
 	  
 Third step: (show conservativity)
 -----------
@@ -84,7 +84,7 @@
 
 def_g g  = 
          (? f. is_f f  & 
-	      g = (LAM x. cfst`(f`<x,fix`(LAM k.csnd`(f`<x,k>))>)) )
+	      g = (LAM x. cfst$(f$<x,fix$(LAM k.csnd$(f$<x,k>))>)) )
 	
 Now we prove:
 
@@ -118,19 +118,19 @@
 defs
 
 is_f		"is_f f == (!i1 i2 o1 o2.
-			f`<i1,i2> = <o1,o2> --> Rf(i1,i2,o1,o2))"
+			f$<i1,i2> = <o1,o2> --> Rf(i1,i2,o1,o2))"
 
 is_net_g	"is_net_g f x y == (? z. 
-			<y,z> = f`<x,z> &
-			(!oy hz. <oy,hz> = f`<x,hz> --> z << hz))" 
+			<y,z> = f$<x,z> &
+			(!oy hz. <oy,hz> = f$<x,hz> --> z << hz))" 
 
 is_g		"is_g g  == (? f.
 			is_f f  & 
-			(!x y. g`x = y --> is_net_g f x y))"
+			(!x y. g$x = y --> is_net_g f x y))"
 
 
 def_g		"def_g g == (? f.
 			is_f f  & 
-	      		g = (LAM x. cfst`(f`<x,fix`(LAM  k. csnd`(f`<x,k>))>)))" 
+	      		g = (LAM x. cfst$(f$<x,fix$(LAM  k. csnd$(f$<x,k>))>)))" 
 
 end
diff -r a7897aebbffc -r f4745d77e620 src/HOLCF/ex/Hoare.ML
--- a/src/HOLCF/ex/Hoare.ML	Tue Jan 09 15:32:27 2001 +0100
+++ b/src/HOLCF/ex/Hoare.ML	Tue Jan 09 15:36:30 2001 +0100
@@ -14,21 +14,21 @@
 by (fast_tac HOL_cs 1);
 qed "hoare_lemma2";
 
-Goal " (ALL k. b1`(iterate k g x) = TT) | (EX k. b1`(iterate k g x)~=TT)";
+Goal " (ALL k. b1$(iterate k g x) = TT) | (EX k. b1$(iterate k g x)~=TT)";
 by (fast_tac HOL_cs 1);
 qed "hoare_lemma3";
 
-Goal "(EX k. b1`(iterate k g x) ~= TT) ==> \
-\ EX k. b1`(iterate k g x) = FF | b1`(iterate k g x) = UU";
+Goal "(EX k. b1$(iterate k g x) ~= TT) ==> \
+\ EX k. b1$(iterate k g x) = FF | b1$(iterate k g x) = UU";
 by (etac exE 1);
 by (rtac exI 1);
 by (rtac hoare_lemma2 1);
 by (atac 1);
 qed "hoare_lemma4";
 
-Goal "[|(EX k. b1`(iterate k g x) ~= TT);\
-\   k=Least(%n. b1`(iterate n g x) ~= TT)|] ==> \
-\ b1`(iterate k g x)=FF | b1`(iterate k g x)=UU";
+Goal "[|(EX k. b1$(iterate k g x) ~= TT);\
+\   k=Least(%n. b1$(iterate n g x) ~= TT)|] ==> \
+\ b1$(iterate k g x)=FF | b1$(iterate k g x)=UU";
 by (hyp_subst_tac 1);
 by (rtac hoare_lemma2 1);
 by (etac exE 1);
@@ -45,13 +45,13 @@
 by (resolve_tac dist_eq_tr 1);
 qed "hoare_lemma7";
 
-Goal "[|(EX k. b1`(iterate k g x) ~= TT);\
-\   k=Least(%n. b1`(iterate n g x) ~= TT)|] ==> \
-\ ALL m. m < k --> b1`(iterate m g x)=TT";
+Goal "[|(EX k. b1$(iterate k g x) ~= TT);\
+\   k=Least(%n. b1$(iterate n g x) ~= TT)|] ==> \
+\ ALL m. m < k --> b1$(iterate m g x)=TT";
 by (hyp_subst_tac 1);
 by (etac exE 1);
 by (strip_tac 1);
-by (res_inst_tac [("p","b1`(iterate m g x)")] trE 1);
+by (res_inst_tac [("p","b1$(iterate m g x)")] trE 1);
 by (atac 2);
 by (rtac (le_less_trans RS less_irrefl) 1);
 by (atac 2);
@@ -64,7 +64,7 @@
 qed "hoare_lemma8";
 
 
-Goal "f`(y::'a)=(UU::tr) ==> f`UU = UU";
+Goal "f$(y::'a)=(UU::tr) ==> f$UU = UU";
 by (etac (flat_codom RS disjE) 1);
 by Auto_tac;  
 qed "hoare_lemma28";
@@ -72,28 +72,28 @@
 
 (* ----- access to definitions ----- *)
 
-Goal "p`x = If b1`x then p`(g`x) else x fi";
+Goal "p$x = If b1$x then p$(g$x) else x fi";
 by (fix_tac3 p_def 1);
 by (Simp_tac 1);
 qed "p_def3";
 
-Goal "q`x = If b1`x orelse b2`x then q`(g`x) else x fi";
+Goal "q$x = If b1$x orelse b2$x then q$(g$x) else x fi";
 by (fix_tac3 q_def 1);
 by (Simp_tac 1);
 qed "q_def3";
 
 (** --------- proves about iterations of p and q ---------- **)
 
-Goal "(ALL m. m< Suc k --> b1`(iterate m g x)=TT) -->\
-\  p`(iterate k g x)=p`x";
+Goal "(ALL m. m< Suc k --> b1$(iterate m g x)=TT) -->\
+\  p$(iterate k g x)=p$x";
 by (nat_ind_tac "k" 1);
 by (Simp_tac 1);
 by (Simp_tac 1);
 by (strip_tac 1);
-by (res_inst_tac [("s","p`(iterate k g x)")] trans 1);
+by (res_inst_tac [("s","p$(iterate k g x)")] trans 1);
 by (rtac trans 1);
 by (rtac (p_def3 RS sym) 2);
-by (res_inst_tac [("s","TT"),("t","b1`(iterate k g x)")] ssubst 1);
+by (res_inst_tac [("s","TT"),("t","b1$(iterate k g x)")] ssubst 1);
 by (rtac mp 1);
 by (etac spec 1);
 by (simp_tac (simpset() addsimps [less_Suc_eq]) 1);
@@ -106,16 +106,16 @@
 by (Simp_tac 1);
 qed "hoare_lemma9";
 
-Goal "(ALL m. m< Suc k --> b1`(iterate m g x)=TT) --> \
-\ q`(iterate k g x)=q`x";
+Goal "(ALL m. m< Suc k --> b1$(iterate m g x)=TT) --> \
+\ q$(iterate k g x)=q$x";
 by (nat_ind_tac "k" 1);
 by (Simp_tac 1);
 by (simp_tac (simpset() addsimps [less_Suc_eq]) 1);
 by (strip_tac 1);
-by (res_inst_tac [("s","q`(iterate k g x)")] trans 1);
+by (res_inst_tac [("s","q$(iterate k g x)")] trans 1);
 by (rtac trans 1);
 by (rtac (q_def3 RS sym) 2);
-by (res_inst_tac [("s","TT"),("t","b1`(iterate k g x)")] ssubst 1);
+by (res_inst_tac [("s","TT"),("t","b1$(iterate k g x)")] ssubst 1);
 by (fast_tac HOL_cs 1);
 by (simp_tac HOLCF_ss 1);
 by (etac mp 1);
@@ -123,20 +123,20 @@
 by (fast_tac (HOL_cs addSDs [less_Suc_eq RS iffD1]) 1);
 qed "hoare_lemma24";
 
-(* -------- results about p for case (EX k. b1`(iterate k g x)~=TT) ------- *)
+(* -------- results about p for case (EX k. b1$(iterate k g x)~=TT) ------- *)
 
 
 val hoare_lemma10 = (hoare_lemma8 RS (hoare_lemma9 RS mp));
 (* 
-val hoare_lemma10 = "[| EX k. b1`(iterate k g ?x1) ~= TT;
-    Suc ?k3 = Least(%n. b1`(iterate n g ?x1) ~= TT) |] ==>
- p`(iterate ?k3 g ?x1) = p`?x1" : thm
+val hoare_lemma10 = "[| EX k. b1$(iterate k g ?x1) ~= TT;
+    Suc ?k3 = Least(%n. b1$(iterate n g ?x1) ~= TT) |] ==>
+ p$(iterate ?k3 g ?x1) = p$?x1" : thm
 
 *)
 
-Goal "(EX n. b1`(iterate n g x) ~= TT) ==>\
-\ k=(LEAST n. b1`(iterate n g x) ~= TT) & b1`(iterate k g x)=FF \
-\ --> p`x = iterate k g x";
+Goal "(EX n. b1$(iterate n g x) ~= TT) ==>\
+\ k=(LEAST n. b1$(iterate n g x) ~= TT) & b1$(iterate k g x)=FF \
+\ --> p$x = iterate k g x";
 by (case_tac "k" 1);
 by (hyp_subst_tac 1);
 by (Simp_tac 1);
@@ -153,7 +153,7 @@
 by (atac 1);
 by (rtac trans 1);
 by (rtac p_def3 1);
-by (res_inst_tac [("s","TT"),("t","b1`(iterate nat g x)")] ssubst 1);
+by (res_inst_tac [("s","TT"),("t","b1$(iterate nat g x)")] ssubst 1);
 by (rtac (hoare_lemma8 RS spec RS mp) 1);
 by (atac 1);
 by (atac 1);
@@ -166,9 +166,9 @@
 by (simp_tac HOLCF_ss 1);
 qed "hoare_lemma11";
 
-Goal "(EX n. b1`(iterate n g x) ~= TT) ==>\
-\ k=Least(%n. b1`(iterate n g x)~=TT) & b1`(iterate k g x)=UU \
-\ --> p`x = UU";
+Goal "(EX n. b1$(iterate n g x) ~= TT) ==>\
+\ k=Least(%n. b1$(iterate n g x)~=TT) & b1$(iterate k g x)=UU \
+\ --> p$x = UU";
 by (case_tac "k" 1);
 by (hyp_subst_tac 1);
 by (Simp_tac 1);
@@ -187,7 +187,7 @@
 by (atac 1);
 by (rtac trans 1);
 by (rtac p_def3 1);
-by (res_inst_tac [("s","TT"),("t","b1`(iterate nat g x)")] ssubst 1);
+by (res_inst_tac [("s","TT"),("t","b1$(iterate nat g x)")] ssubst 1);
 by (rtac (hoare_lemma8 RS spec RS mp) 1);
 by (atac 1);
 by (atac 1);
@@ -198,9 +198,9 @@
 by (asm_simp_tac HOLCF_ss 1);
 qed "hoare_lemma12";
 
-(* -------- results about p for case  (ALL k. b1`(iterate k g x)=TT) ------- *)
+(* -------- results about p for case  (ALL k. b1$(iterate k g x)=TT) ------- *)
 
-Goal "(ALL k. b1`(iterate k g x)=TT) ==> ALL k. p`(iterate k g x) = UU";
+Goal "(ALL k. b1$(iterate k g x)=TT) ==> ALL k. p$(iterate k g x) = UU";
 by (rtac (p_def RS def_fix_ind) 1);
 by (rtac adm_all 1);
 by (rtac allI 1);
@@ -211,21 +211,21 @@
 by (rtac refl 1);
 by (Simp_tac 1);
 by (rtac allI 1);
-by (res_inst_tac [("s","TT"),("t","b1`(iterate k g x)")] ssubst 1);
+by (res_inst_tac [("s","TT"),("t","b1$(iterate k g x)")] ssubst 1);
 by (etac spec 1);
 by (asm_simp_tac HOLCF_ss 1);
 by (rtac (iterate_Suc RS subst) 1);
 by (etac spec 1);
 qed "fernpass_lemma";
 
-Goal "(ALL k. b1`(iterate k g x)=TT) ==> p`x = UU";
+Goal "(ALL k. b1$(iterate k g x)=TT) ==> p$x = UU";
 by (res_inst_tac [("F1","g"),("t","x")] (iterate_0 RS subst) 1);
 by (etac (fernpass_lemma RS spec) 1);
 qed "hoare_lemma16";
 
-(* -------- results about q for case  (ALL k. b1`(iterate k g x)=TT) ------- *)
+(* -------- results about q for case  (ALL k. b1$(iterate k g x)=TT) ------- *)
 
-Goal "(ALL k. b1`(iterate k g x)=TT) ==> ALL k. q`(iterate k g x) = UU";
+Goal "(ALL k. b1$(iterate k g x)=TT) ==> ALL k. q$(iterate k g x) = UU";
 by (rtac (q_def RS def_fix_ind) 1);
 by (rtac adm_all 1);
 by (rtac allI 1);
@@ -236,25 +236,25 @@
 by (rtac refl 1);
 by (rtac allI 1);
 by (Simp_tac 1);
-by (res_inst_tac [("s","TT"),("t","b1`(iterate k g x)")] ssubst 1);
+by (res_inst_tac [("s","TT"),("t","b1$(iterate k g x)")] ssubst 1);
 by (etac spec 1);
 by (asm_simp_tac HOLCF_ss 1);
 by (rtac (iterate_Suc RS subst) 1);
 by (etac spec 1);
 qed "hoare_lemma17";
 
-Goal "(ALL k. b1`(iterate k g x)=TT) ==> q`x = UU";
+Goal "(ALL k. b1$(iterate k g x)=TT) ==> q$x = UU";
 by (res_inst_tac [("F1","g"),("t","x")] (iterate_0 RS subst) 1);
 by (etac (hoare_lemma17 RS spec) 1);
 qed "hoare_lemma18";
 
-Goal "(ALL k. (b1::'a->tr)`(iterate k g x)=TT) ==> b1`(UU::'a) = UU | (ALL y. b1`(y::'a)=TT)";
+Goal "(ALL k. (b1::'a->tr)$(iterate k g x)=TT) ==> b1$(UU::'a) = UU | (ALL y. b1$(y::'a)=TT)";
 by (rtac (flat_codom) 1);
 by (res_inst_tac [("t","x1")] (iterate_0 RS subst) 1);
 by (etac spec 1);
 qed "hoare_lemma19";
 
-Goal "(ALL y. b1`(y::'a)=TT) ==> ALL k. q`(iterate k g (x::'a)) = UU";
+Goal "(ALL y. b1$(y::'a)=TT) ==> ALL k. q$(iterate k g (x::'a)) = UU";
 by (rtac (q_def RS def_fix_ind) 1);
 by (rtac adm_all 1);
 by (rtac allI 1);
@@ -265,35 +265,35 @@
 by (rtac refl 1);
 by (rtac allI 1);
 by (Simp_tac 1);
-by (res_inst_tac [("s","TT"),("t","b1`(iterate k g (x::'a))")] ssubst 1);
+by (res_inst_tac [("s","TT"),("t","b1$(iterate k g (x::'a))")] ssubst 1);
 by (etac spec 1);
 by (asm_simp_tac HOLCF_ss 1);
 by (rtac (iterate_Suc RS subst) 1);
 by (etac spec 1);
 qed "hoare_lemma20";
 
-Goal "(ALL y. b1`(y::'a)=TT) ==> q`(x::'a) = UU";
+Goal "(ALL y. b1$(y::'a)=TT) ==> q$(x::'a) = UU";
 by (res_inst_tac [("F1","g"),("t","x")] (iterate_0 RS subst) 1);
 by (etac (hoare_lemma20 RS spec) 1);
 qed "hoare_lemma21";
 
-Goal "b1`(UU::'a)=UU ==> q`(UU::'a) = UU";
+Goal "b1$(UU::'a)=UU ==> q$(UU::'a) = UU";
 by (stac q_def3 1);
 by (asm_simp_tac HOLCF_ss 1);
 qed "hoare_lemma22";
 
-(* -------- results about q for case (EX k. b1`(iterate k g x) ~= TT) ------- *)
+(* -------- results about q for case (EX k. b1$(iterate k g x) ~= TT) ------- *)
 
 val hoare_lemma25 = (hoare_lemma8 RS (hoare_lemma24 RS mp) );
 (* 
-val hoare_lemma25 = "[| EX k. b1`(iterate k g ?x1) ~= TT;
-    Suc ?k3 = Least(%n. b1`(iterate n g ?x1) ~= TT) |] ==>
- q`(iterate ?k3 g ?x1) = q`?x1" : thm
+val hoare_lemma25 = "[| EX k. b1$(iterate k g ?x1) ~= TT;
+    Suc ?k3 = Least(%n. b1$(iterate n g ?x1) ~= TT) |] ==>
+ q$(iterate ?k3 g ?x1) = q$?x1" : thm
 *)
 
-Goal "(EX n. b1`(iterate n g x)~=TT) ==>\
-\ k=Least(%n. b1`(iterate n g x) ~= TT) & b1`(iterate k g x) =FF \
-\ --> q`x = q`(iterate k g x)";
+Goal "(EX n. b1$(iterate n g x)~=TT) ==>\
+\ k=Least(%n. b1$(iterate n g x) ~= TT) & b1$(iterate k g x) =FF \
+\ --> q$x = q$(iterate k g x)";
 by (case_tac "k" 1);
 by (hyp_subst_tac 1);
 by (strip_tac 1);
@@ -307,7 +307,7 @@
 by (atac 1);
 by (rtac trans 1);
 by (rtac q_def3 1);
-by (res_inst_tac [("s","TT"),("t","b1`(iterate nat g x)")] ssubst 1);
+by (res_inst_tac [("s","TT"),("t","b1$(iterate nat g x)")] ssubst 1);
 by (rtac (hoare_lemma8 RS spec RS mp) 1);
 by (atac 1);
 by (atac 1);
@@ -316,9 +316,9 @@
 qed "hoare_lemma26";
 
 
-Goal "(EX n. b1`(iterate n g x) ~= TT) ==>\
-\ k=Least(%n. b1`(iterate n g x)~=TT) & b1`(iterate k g x)=UU \
-\ --> q`x = UU";
+Goal "(EX n. b1$(iterate n g x) ~= TT) ==>\
+\ k=Least(%n. b1$(iterate n g x)~=TT) & b1$(iterate k g x)=UU \
+\ --> q$x = UU";
 by (case_tac "k" 1);
 by (hyp_subst_tac 1);
 by (Simp_tac 1);
@@ -336,7 +336,7 @@
 by (atac 1);
 by (rtac trans 1);
 by (rtac q_def3 1);
-by (res_inst_tac [("s","TT"),("t","b1`(iterate nat g x)")] ssubst 1);
+by (res_inst_tac [("s","TT"),("t","b1$(iterate nat g x)")] ssubst 1);
 by (rtac (hoare_lemma8 RS spec RS mp) 1);
 by (atac 1);
 by (atac 1);
@@ -347,9 +347,9 @@
 by (asm_simp_tac HOLCF_ss 1);
 qed "hoare_lemma27";
 
-(* ------- (ALL k. b1`(iterate k g x)=TT) ==> q o p = q   ----- *)
+(* ------- (ALL k. b1$(iterate k g x)=TT) ==> q o p = q   ----- *)
 
-Goal "(ALL k. b1`(iterate k g x)=TT) ==> q`(p`x) = q`x";
+Goal "(ALL k. b1$(iterate k g x)=TT) ==> q$(p$x) = q$x";
 by (stac hoare_lemma16 1);
 by (atac 1);
 by (rtac (hoare_lemma19 RS disjE) 1);
@@ -368,7 +368,7 @@
 
 (* ------------  EX k. b1~(iterate k g x) ~= TT ==> q o p = q   ----- *)
 
-Goal "EX k. b1`(iterate k g x) ~= TT ==> q`(p`x) = q`x";
+Goal "EX k. b1$(iterate k g x) ~= TT ==> q$(p$x) = q$x";
 by (rtac (hoare_lemma5 RS disjE) 1);
 by (atac 1);
 by (rtac refl 1);
diff -r a7897aebbffc -r f4745d77e620 src/HOLCF/ex/Hoare.thy
--- a/src/HOLCF/ex/Hoare.thy	Tue Jan 09 15:32:27 2001 +0100
+++ b/src/HOLCF/ex/Hoare.thy	Tue Jan 09 15:36:30 2001 +0100
@@ -32,11 +32,11 @@
 
 defs
 
-  p_def  "p == fix`(LAM f. LAM x.
-                 If b1`x then f`(g`x) else x fi)"
+  p_def  "p == fix$(LAM f. LAM x.
+                 If b1$x then f$(g$x) else x fi)"
 
-  q_def  "q == fix`(LAM f. LAM x.
-                 If b1`x orelse b2`x then f`(g`x) else x fi)"
+  q_def  "q == fix$(LAM f. LAM x.
+                 If b1$x orelse b2$x then f$(g$x) else x fi)"
 
 end
  
diff -r a7897aebbffc -r f4745d77e620 src/HOLCF/ex/Loop.ML
--- a/src/HOLCF/ex/Loop.ML	Tue Jan 09 15:32:27 2001 +0100
+++ b/src/HOLCF/ex/Loop.ML	Tue Jan 09 15:36:30 2001 +0100
@@ -11,11 +11,11 @@
 (* ------------------------------------------------------------------------- *)
 
 
-Goalw [step_def] "step`b`g`x = If b`x then g`x else x fi";
+Goalw [step_def] "step$b$g$x = If b$x then g$x else x fi";
 by (Simp_tac 1);
 qed "step_def2";
 
-Goalw [while_def] "while`b`g = fix`(LAM f x. If b`x then f`(g`x) else x fi)";
+Goalw [while_def] "while$b$g = fix$(LAM f x. If b$x then f$(g$x) else x fi)";
 by (Simp_tac 1);
 qed "while_def2";
 
@@ -24,12 +24,12 @@
 (* rekursive properties of while                                             *)
 (* ------------------------------------------------------------------------- *)
 
-Goal "while`b`g`x = If b`x then while`b`g`(g`x) else x fi";
+Goal "while$b$g$x = If b$x then while$b$g$(g$x) else x fi";
 by (fix_tac5  while_def2 1);
 by (Simp_tac 1);
 qed "while_unfold";
 
-Goal "ALL x. while`b`g`x = while`b`g`(iterate k (step`b`g) x)";
+Goal "ALL x. while$b$g$x = while$b$g$(iterate k (step$b$g) x)";
 by (nat_ind_tac "k" 1);
 by (simp_tac HOLCF_ss 1);
 by (rtac allI 1);
@@ -40,10 +40,10 @@
 by (rtac trans 1);
 by (etac spec 2);
 by (stac step_def2 1);
-by (res_inst_tac [("p","b`x")] trE 1);
+by (res_inst_tac [("p","b$x")] trE 1);
 by (asm_simp_tac HOLCF_ss 1);
 by (stac while_unfold 1);
-by (res_inst_tac [("s","UU"),("t","b`UU")]ssubst 1);
+by (res_inst_tac [("s","UU"),("t","b$UU")]ssubst 1);
 by (etac (flat_codom RS disjE) 1);
 by (atac 1);
 by (etac spec 1);
@@ -54,8 +54,8 @@
 by (asm_simp_tac HOLCF_ss 1);
 qed "while_unfold2";
 
-Goal "while`b`g`x = while`b`g`(step`b`g`x)";
-by (res_inst_tac [("s", "while`b`g`(iterate (Suc 0) (step`b`g) x)")] trans 1);
+Goal "while$b$g$x = while$b$g$(step$b$g$x)";
+by (res_inst_tac [("s", "while$b$g$(iterate (Suc 0) (step$b$g) x)")] trans 1);
 by (rtac (while_unfold2 RS spec) 1);
 by (Simp_tac 1);
 qed "while_unfold3";
@@ -65,8 +65,8 @@
 (* properties of while and iterations                                        *)
 (* ------------------------------------------------------------------------- *)
 
-Goal "[| EX y. b`y=FF; iterate k (step`b`g) x = UU |] \
-\    ==>iterate(Suc k) (step`b`g) x=UU";
+Goal "[| EX y. b$y=FF; iterate k (step$b$g) x = UU |] \
+\    ==>iterate(Suc k) (step$b$g) x=UU";
 by (Simp_tac 1);
 by (rtac trans 1);
 by (rtac step_def2 1);
@@ -77,34 +77,34 @@
 by (asm_simp_tac HOLCF_ss 1);
 qed "loop_lemma1";
 
-Goal "[|EX y. b`y=FF;iterate (Suc k) (step`b`g) x ~=UU |]==>\
-\     iterate k (step`b`g) x ~=UU";
+Goal "[|EX y. b$y=FF;iterate (Suc k) (step$b$g) x ~=UU |]==>\
+\     iterate k (step$b$g) x ~=UU";
 
 by (blast_tac (claset() addIs [loop_lemma1]) 1);
 qed "loop_lemma2";
 
-Goal "[| ALL x. INV x & b`x=TT & g`x~=UU --> INV (g`x);\
-\        EX y. b`y=FF; INV x |] \
-\     ==> iterate k (step`b`g) x ~=UU --> INV (iterate k (step`b`g) x)";
+Goal "[| ALL x. INV x & b$x=TT & g$x~=UU --> INV (g$x);\
+\        EX y. b$y=FF; INV x |] \
+\     ==> iterate k (step$b$g) x ~=UU --> INV (iterate k (step$b$g) x)";
 by (nat_ind_tac "k" 1);
 by (Asm_simp_tac 1);
 by (strip_tac 1);
 by (simp_tac (simpset() addsimps [step_def2]) 1);
-by (res_inst_tac [("p","b`(iterate k (step`b`g) x)")] trE 1);
+by (res_inst_tac [("p","b$(iterate k (step$b$g) x)")] trE 1);
 by (etac notE 1);
 by (asm_simp_tac (HOLCF_ss addsimps [step_def2] ) 1);
 by (asm_simp_tac HOLCF_ss 1);
 by (rtac mp 1);
 by (etac spec 1);
 by (asm_simp_tac (HOLCF_ss delsimps [iterate_Suc] addsimps [loop_lemma2] ) 1);
-by (res_inst_tac [("s","iterate (Suc k) (step`b`g) x"),
-                  ("t","g`(iterate k (step`b`g) x)")] ssubst 1);
+by (res_inst_tac [("s","iterate (Suc k) (step$b$g) x"),
+                  ("t","g$(iterate k (step$b$g) x)")] ssubst 1);
 by (atac 2);
 by (asm_simp_tac (HOLCF_ss addsimps [step_def2] ) 1);
 by (asm_simp_tac (HOLCF_ss delsimps [iterate_Suc] addsimps [loop_lemma2] ) 1);
 qed_spec_mp "loop_lemma3";
 
-Goal "ALL x. b`(iterate k (step`b`g) x)=FF --> while`b`g`x= iterate k (step`b`g) x";
+Goal "ALL x. b$(iterate k (step$b$g) x)=FF --> while$b$g$x= iterate k (step$b$g) x";
 by (nat_ind_tac "k" 1);
 by (Simp_tac 1);
 by (strip_tac 1);
@@ -118,8 +118,8 @@
 by (Asm_simp_tac 1);
 qed_spec_mp "loop_lemma4";
 
-Goal "ALL k. b`(iterate k (step`b`g) x) ~= FF ==>\
-\ ALL m. while`b`g`(iterate m (step`b`g) x)=UU";
+Goal "ALL k. b$(iterate k (step$b$g) x) ~= FF ==>\
+\ ALL m. while$b$g$(iterate m (step$b$g) x)=UU";
 by (stac while_def2 1);
 by (rtac fix_ind 1);
 by (rtac (allI RS adm_all) 1);
@@ -128,10 +128,10 @@
 by (Simp_tac  1);
 by (rtac allI 1);
 by (Simp_tac  1);
-by (res_inst_tac [("p","b`(iterate m (step`b`g) x)")] trE 1);
+by (res_inst_tac [("p","b$(iterate m (step$b$g) x)")] trE 1);
 by (Asm_simp_tac 1);
 by (Asm_simp_tac 1);
-by (res_inst_tac [("s","xa`(iterate (Suc m) (step`b`g) x)")] trans 1);
+by (res_inst_tac [("s","xa$(iterate (Suc m) (step$b$g) x)")] trans 1);
 by (etac spec 2);
 by (rtac cfun_arg_cong 1);
 by (rtac trans 1);
@@ -141,12 +141,12 @@
 qed_spec_mp "loop_lemma5";
 
 
-Goal "ALL k. b`(iterate k (step`b`g) x) ~= FF ==> while`b`g`x=UU";
+Goal "ALL k. b$(iterate k (step$b$g) x) ~= FF ==> while$b$g$x=UU";
 by (res_inst_tac [("t","x")] (iterate_0 RS subst) 1);
 by (etac (loop_lemma5) 1);
 qed "loop_lemma6";
 
-Goal "while`b`g`x ~= UU ==> EX k. b`(iterate k (step`b`g) x) = FF";
+Goal "while$b$g$x ~= UU ==> EX k. b$(iterate k (step$b$g) x) = FF";
 by (blast_tac (claset() addIs [loop_lemma6]) 1);
 qed "loop_lemma7";
 
@@ -156,10 +156,10 @@
 (* ------------------------------------------------------------------------- *)
 
 Goal
-"[| (ALL y. INV y & b`y=TT & g`y ~= UU --> INV (g`y));\
-\   (ALL y. INV y & b`y=FF --> Q y);\
-\   INV x; while`b`g`x~=UU |] ==> Q (while`b`g`x)";
-by (res_inst_tac [("P","%k. b`(iterate k (step`b`g) x)=FF")] exE 1);
+"[| (ALL y. INV y & b$y=TT & g$y ~= UU --> INV (g$y));\
+\   (ALL y. INV y & b$y=FF --> Q y);\
+\   INV x; while$b$g$x~=UU |] ==> Q (while$b$g$x)";
+by (res_inst_tac [("P","%k. b$(iterate k (step$b$g) x)=FF")] exE 1);
 by (etac loop_lemma7 1);
 by (stac (loop_lemma4) 1);
 by (atac 1);
@@ -177,9 +177,9 @@
 val [premP,premI,premTT,premFF,premW] = Goal
 "[| P(x); \
 \   !!y. P y ==> INV y;\
-\   !!y. [| INV y; b`y=TT; g`y~=UU|] ==> INV (g`y);\
-\   !!y. [| INV y; b`y=FF|] ==> Q y;\
-\   while`b`g`x ~= UU |] ==> Q (while`b`g`x)";
+\   !!y. [| INV y; b$y=TT; g$y~=UU|] ==> INV (g$y);\
+\   !!y. [| INV y; b$y=FF|] ==> Q y;\
+\   while$b$g$x ~= UU |] ==> Q (while$b$g$x)";
 by (rtac loop_inv2 1);
 by (rtac (premP RS premI) 3);
 by (rtac premW 3);
diff -r a7897aebbffc -r f4745d77e620 src/HOLCF/ex/Loop.thy
--- a/src/HOLCF/ex/Loop.thy	Tue Jan 09 15:32:27 2001 +0100
+++ b/src/HOLCF/ex/Loop.thy	Tue Jan 09 15:36:30 2001 +0100
@@ -14,9 +14,9 @@
 
 defs
 
-  step_def      "step == (LAM b g x. If b`x then g`x else x fi)"
-  while_def     "while == (LAM b g. fix`(LAM f x.
-                   If b`x then f`(g`x) else x fi))"
+  step_def      "step == (LAM b g x. If b$x then g$x else x fi)"
+  while_def     "while == (LAM b g. fix$(LAM f x.
+                   If b$x then f$(g$x) else x fi))"
 
 end
  
diff -r a7897aebbffc -r f4745d77e620 src/HOLCF/ex/Stream.ML
--- a/src/HOLCF/ex/Stream.ML	Tue Jan 09 15:32:27 2001 +0100
+++ b/src/HOLCF/ex/Stream.ML	Tue Jan 09 15:36:30 2001 +0100
@@ -74,7 +74,7 @@
 
 section "stream_when";
 
-Goal "stream_when`UU`s=UU";
+Goal "stream_when$UU$s=UU";
 by (stream_case_tac "s" 1);
 by (ALLGOALS(asm_simp_tac (simpset() addsimps [strict_Rep_CFun1])));
 qed "stream_when_strictf";
@@ -87,23 +87,23 @@
 section "ft & rt";
 
 (*
-Goal "ft`s=UU --> s=UU";
+Goal "ft$s=UU --> s=UU";
 by (stream_case_tac "s" 1);
 by (REPEAT (asm_simp_tac (simpset() addsimps stream.rews) 1));
 qed "stream_ft_lemma1";
 *)
 
-Goal "s~=UU ==> ft`s~=UU";
+Goal "s~=UU ==> ft$s~=UU";
 by (stream_case_tac "s" 1);
 by (Blast_tac 1);
 by (asm_simp_tac (simpset() addsimps stream.rews) 1);
 qed "ft_defin";
 
-Goal "rt`s~=UU ==> s~=UU";
+Goal "rt$s~=UU ==> s~=UU";
 by Auto_tac;
 qed "rt_strict_rev";
 
-Goal "(ft`s)&&(rt`s)=s";
+Goal "(ft$s)&&(rt$s)=s";
 by (stream_case_tac "s" 1);
 by (ALLGOALS (asm_simp_tac (simpset() addsimps stream.rews)));
 qed "surjectiv_scons";
@@ -127,16 +127,16 @@
 
 section "stream_take";
 
-Goal  "(LUB i. stream_take i`s) = s";
-by (subgoal_tac "(LUB i. stream_take i`s) = fix`stream_copy`s" 1);
+Goal  "(LUB i. stream_take i$s) = s";
+by (subgoal_tac "(LUB i. stream_take i$s) = fix$stream_copy$s" 1);
 by (simp_tac (simpset() addsimps [fix_def2, stream.take_def,
                                   contlub_cfun_fun, chain_iterate]) 2);
 by (asm_full_simp_tac (simpset() addsimps [stream.reach]) 1);
 qed "stream_reach2";
 
-Goal "chain (%i. stream_take i`s)";
+Goal "chain (%i. stream_take i$s)";
 by (rtac chainI 1);
-by (subgoal_tac "ALL i s. stream_take i`s << stream_take (Suc i)`s" 1);
+by (subgoal_tac "ALL i s. stream_take i$s << stream_take (Suc i)$s" 1);
 by (Fast_tac 1);
 by (rtac allI 1);
 by (induct_tac "ia" 1);
@@ -149,9 +149,9 @@
 
 
 Goalw [stream.take_def]
-	"stream_take n`x = x ==> stream_take (Suc n)`x = x";
+	"stream_take n$x = x ==> stream_take (Suc n)$x = x";
 by (rtac antisym_less 1);
-by (subgoal_tac "iterate (Suc n) stream_copy UU`x << fix`stream_copy`x" 1);
+by (subgoal_tac "iterate (Suc n) stream_copy UU$x << fix$stream_copy$x" 1);
 by (asm_full_simp_tac (simpset() addsimps [stream.reach]) 1);
 by (rtac monofun_cfun_fun 1);
 by (stac fix_def2 1);
@@ -163,7 +163,7 @@
 
 (*
 Goal 
- "ALL  s2. stream_take n`s2 = s2 --> stream_take (Suc n)`s2=s2";
+ "ALL  s2. stream_take n$s2 = s2 --> stream_take (Suc n)$s2=s2";
 by (induct_tac "n" 1);
 by (simp_tac (simpset() addsimps stream_rews) 1);
 by (strip_tac 1);
@@ -174,7 +174,7 @@
 by (asm_simp_tac (simpset() addsimps stream_rews) 1);
 by (asm_simp_tac (simpset() addsimps stream_rews) 1);
 by (strip_tac 1 );
-by (subgoal_tac "stream_take n1`xs = xs" 1);
+by (subgoal_tac "stream_take n1$xs = xs" 1);
 by (rtac ((hd stream_inject) RS conjunct2) 2);
 by (atac 4);
 by (atac 2);
@@ -185,7 +185,7 @@
 *)
 
 Goal 
- "ALL x xs. x~=UU --> stream_take n`(x && xs) = x && xs --> stream_take n`xs=xs";
+ "ALL x xs. x~=UU --> stream_take n$(x && xs) = x && xs --> stream_take n$xs=xs";
 by (induct_tac "n" 1);
 by (Asm_simp_tac 1);
 by (strip_tac 1);
@@ -201,7 +201,7 @@
 qed_spec_mp "stream_take_lemma3";
 
 Goal 
- "ALL x xs. stream_take n`xs=xs --> stream_take (Suc n)`(x && xs) = x && xs";
+ "ALL x xs. stream_take n$xs=xs --> stream_take (Suc n)$(x && xs) = x && xs";
 by (induct_tac "n" 1);
 by Auto_tac;  
 qed_spec_mp "stream_take_lemma4";
@@ -232,7 +232,7 @@
 "[| P UU;\
 \   !! x    .    x ~= UU                  ==> P (x      && UU); \
 \   !! y z s. [| y ~= UU; z ~= UU; P s |] ==> P (y && z && s )  \
-\   |] ==> !s. P (stream_take n`s)";
+\   |] ==> !s. P (stream_take n$s)";
 by (res_inst_tac [("n","n")] nat_induct2 1);
 by (asm_simp_tac (simpset() addsimps [major]) 1);
 by (rtac allI 1);
@@ -275,7 +275,7 @@
 
 
 Goalw [stream.bisim_def]
-"!s1 s2. R s1 s2 --> ft`s1 = ft`s2 &  R (rt`s1) (rt`s2) ==> stream_bisim R";
+"!s1 s2. R s1 s2 --> ft$s1 = ft$s2 &  R (rt$s1) (rt$s2) ==> stream_bisim R";
 by (strip_tac 1);
 by (etac allE 1);
 by (etac allE 1);
@@ -288,21 +288,21 @@
 by (rtac disjI2 1);
 by (rtac disjE 1);
 by (etac (de_Morgan_conj RS subst) 1);
-by (res_inst_tac [("x","ft`x")] exI 1);
-by (res_inst_tac [("x","rt`x")] exI 1);
-by (res_inst_tac [("x","rt`x'")] exI 1);
+by (res_inst_tac [("x","ft$x")] exI 1);
+by (res_inst_tac [("x","rt$x")] exI 1);
+by (res_inst_tac [("x","rt$x'")] exI 1);
 by (rtac conjI 1);
 by (etac ft_defin 1);
 by (asm_simp_tac (simpset() addsimps stream.rews addsimps [surjectiv_scons]) 1);
-by (eres_inst_tac [("s","ft`x"),("t","ft`x'")] subst 1);
+by (eres_inst_tac [("s","ft$x"),("t","ft$x'")] subst 1);
 by (simp_tac (simpset() addsimps stream.rews addsimps [surjectiv_scons]) 1);
-by (res_inst_tac [("x","ft`x'")] exI 1);
-by (res_inst_tac [("x","rt`x")] exI 1);
-by (res_inst_tac [("x","rt`x'")] exI 1);
+by (res_inst_tac [("x","ft$x'")] exI 1);
+by (res_inst_tac [("x","rt$x")] exI 1);
+by (res_inst_tac [("x","rt$x'")] exI 1);
 by (rtac conjI 1);
 by (etac ft_defin 1);
 by (asm_simp_tac (simpset() addsimps stream.rews addsimps [surjectiv_scons]) 1);
-by (res_inst_tac [("s","ft`x"),("t","ft`x'")] ssubst 1);
+by (res_inst_tac [("s","ft$x"),("t","ft$x'")] ssubst 1);
 by (etac sym 1);
 by (simp_tac (simpset() addsimps stream.rews addsimps [surjectiv_scons]) 1);
 qed "stream_coind_lemma2";
@@ -332,7 +332,7 @@
 by (blast_tac (claset() addIs [stream_take_lemma3]) 1);
 qed "stream_finite_lemma2";
 
-Goal "stream_finite (rt`s) = stream_finite s";
+Goal "stream_finite (rt$s) = stream_finite s";
 by (stream_case_tac "s" 1);
 by (simp_tac (simpset() addsimps [stream_finite_UU]) 1);
 by (Asm_simp_tac 1);
diff -r a7897aebbffc -r f4745d77e620 src/HOLCF/ex/loeckx.ML
--- a/src/HOLCF/ex/loeckx.ML	Tue Jan 09 15:32:27 2001 +0100
+++ b/src/HOLCF/ex/loeckx.ML	Tue Jan 09 15:36:30 2001 +0100
@@ -19,16 +19,16 @@
 Since we already proved the theorem
 
 val cont_lubcfun = prove_goal Cfun2.thy 
-        "chain ?F ==> cont (%x. lub (range (%j. ?F j`x)))"
+        "chain ?F ==> cont (%x. lub (range (%j. ?F j$x)))"
 
 
 it suffices to prove:
 
-Ifix  = (%f.lub (range (%j. (LAM f. iterate j f UU)`f)))
+Ifix  = (%f.lub (range (%j. (LAM f. iterate j f UU)$f)))
 
 and 
 
-cont (%f.lub (range (%j. (LAM f. iterate j f UU)`f)))
+cont (%f.lub (range (%j. (LAM f. iterate j f UU)$f)))
 
 Note that if we use the term 
 
@@ -40,15 +40,15 @@
 
 Goal "cont(Ifix)";
 by (res_inst_tac 
- [("t","Ifix"),("s","(%f. lub(range(%j.(LAM f. iterate j f UU)`f)))")]
+ [("t","Ifix"),("s","(%f. lub(range(%j.(LAM f. iterate j f UU)$f)))")]
   ssubst 1);
 by (rtac ext 1);
 by (rewtac Ifix_def );
 by (subgoal_tac 
-  "range(% i. iterate i f UU) = range(%j.(LAM f. iterate j f UU)`f)" 1);
+  "range(% i. iterate i f UU) = range(%j.(LAM f. iterate j f UU)$f)" 1);
 by (etac arg_cong 1);
 by (subgoal_tac 
-        "(% i. iterate i f UU) = (%j.(LAM f. iterate j f UU)`f)" 1);
+        "(% i. iterate i f UU) = (%j.(LAM f. iterate j f UU)$f)" 1);
 by (etac arg_cong 1);
 by (rtac ext 1);
 by (stac beta_cfun 1);
@@ -70,19 +70,19 @@
 
 (* the proof in little steps *)
 
-Goal "(% i. iterate i f UU) = (%j.(LAM f. iterate j f UU)`f)";
+Goal "(% i. iterate i f UU) = (%j.(LAM f. iterate j f UU)$f)";
 by (rtac ext 1);
 by (simp_tac (simpset() addsimps [beta_cfun, cont2cont_CF1L, cont_iterate]) 1);
 qed "fix_lemma1";
 
-Goal "Ifix = (%f. lub(range(%j.(LAM f. iterate j f UU)`f)))";
+Goal "Ifix = (%f. lub(range(%j.(LAM f. iterate j f UU)$f)))";
 by (rtac ext 1);
 by (simp_tac (simpset() addsimps [Ifix_def, fix_lemma1]) 1);
 qed "fix_lemma2";
 
 (*
 - cont_lubcfun;
-val it = "chain ?F ==> cont (%x. lub (range (%j. ?F j`x)))" : thm   
+val it = "chain ?F ==> cont (%x. lub (range (%j. ?F j$x)))" : thm   
 
 *)