` -> $
authornipkow
Tue Jan 09 15:36:30 2001 +0100 (2001-01-09)
changeset 10835f4745d77e620
parent 10834 a7897aebbffc
child 10836 666621128f5a
` -> $
src/HOLCF/IMP/Denotational.ML
src/HOLCF/IMP/Denotational.thy
src/HOLCF/IMP/HoareEx.thy
src/HOLCF/IOA/meta_theory/Abstraction.ML
src/HOLCF/IOA/meta_theory/Abstraction.thy
src/HOLCF/IOA/meta_theory/CompoExecs.ML
src/HOLCF/IOA/meta_theory/CompoExecs.thy
src/HOLCF/IOA/meta_theory/CompoScheds.ML
src/HOLCF/IOA/meta_theory/CompoScheds.thy
src/HOLCF/IOA/meta_theory/CompoTraces.ML
src/HOLCF/IOA/meta_theory/CompoTraces.thy
src/HOLCF/IOA/meta_theory/Compositionality.ML
src/HOLCF/IOA/meta_theory/Deadlock.ML
src/HOLCF/IOA/meta_theory/LiveIOA.thy
src/HOLCF/IOA/meta_theory/RefCorrectness.ML
src/HOLCF/IOA/meta_theory/RefCorrectness.thy
src/HOLCF/IOA/meta_theory/RefMappings.thy
src/HOLCF/IOA/meta_theory/Seq.ML
src/HOLCF/IOA/meta_theory/Seq.thy
src/HOLCF/IOA/meta_theory/Sequence.ML
src/HOLCF/IOA/meta_theory/Sequence.thy
src/HOLCF/IOA/meta_theory/ShortExecutions.ML
src/HOLCF/IOA/meta_theory/ShortExecutions.thy
src/HOLCF/IOA/meta_theory/SimCorrectness.ML
src/HOLCF/IOA/meta_theory/SimCorrectness.thy
src/HOLCF/IOA/meta_theory/Simulations.ML
src/HOLCF/IOA/meta_theory/Simulations.thy
src/HOLCF/IOA/meta_theory/TL.ML
src/HOLCF/IOA/meta_theory/TL.thy
src/HOLCF/IOA/meta_theory/TLS.ML
src/HOLCF/IOA/meta_theory/TLS.thy
src/HOLCF/IOA/meta_theory/Traces.ML
src/HOLCF/IOA/meta_theory/Traces.thy
src/HOLCF/domain/theorems.ML
src/HOLCF/ex/Dagstuhl.thy
src/HOLCF/ex/Dnat.ML
src/HOLCF/ex/Dnat.thy
src/HOLCF/ex/Fix2.ML
src/HOLCF/ex/Fix2.thy
src/HOLCF/ex/Focus_ex.ML
src/HOLCF/ex/Focus_ex.thy
src/HOLCF/ex/Hoare.ML
src/HOLCF/ex/Hoare.thy
src/HOLCF/ex/Loop.ML
src/HOLCF/ex/Loop.thy
src/HOLCF/ex/Stream.ML
src/HOLCF/ex/loeckx.ML
     1.1 --- a/src/HOLCF/IMP/Denotational.ML	Tue Jan 09 15:32:27 2001 +0100
     1.2 +++ b/src/HOLCF/IMP/Denotational.ML	Tue Jan 09 15:36:30 2001 +0100
     1.3 @@ -6,7 +6,7 @@
     1.4  Equivalence of Denotational Semantics in HOLCF and Evaluation Semantics in HOL
     1.5  *)
     1.6  
     1.7 -Goalw [dlift_def] "dlift f`(Def x) = f`(Discr x)";
     1.8 +Goalw [dlift_def] "dlift f$(Def x) = f$(Discr x)";
     1.9  by (Simp_tac 1);
    1.10  qed "dlift_Def";
    1.11  Addsimps [dlift_Def];
    1.12 @@ -17,18 +17,18 @@
    1.13  AddIffs [cont_dlift];
    1.14  
    1.15  Goalw [dlift_def]
    1.16 - "(dlift f`l = Def y) = (? x. l = Def x & f`(Discr x) = Def y)";
    1.17 + "(dlift f$l = Def y) = (? x. l = Def x & f$(Discr x) = Def y)";
    1.18  by (simp_tac (simpset() addsplits [Lift1.lift.split]) 1);
    1.19  qed "dlift_is_Def";
    1.20  Addsimps [dlift_is_Def];
    1.21  
    1.22 -Goal "<c,s> -c-> t ==> D c`(Discr s) = (Def t)";
    1.23 +Goal "<c,s> -c-> t ==> D c$(Discr s) = (Def t)";
    1.24  by (etac evalc.induct 1);
    1.25        by (ALLGOALS Asm_simp_tac);
    1.26   by (ALLGOALS (stac fix_eq THEN' Asm_full_simp_tac));
    1.27  qed_spec_mp "eval_implies_D";
    1.28  
    1.29 -Goal "!s t. D c`(Discr s) = (Def t) --> <c,s> -c-> t";
    1.30 +Goal "!s t. D c$(Discr s) = (Def t) --> <c,s> -c-> t";
    1.31  by (induct_tac "c" 1);
    1.32      by (Force_tac 1);
    1.33     by (Force_tac 1);
    1.34 @@ -46,6 +46,6 @@
    1.35  qed_spec_mp "D_implies_eval";
    1.36  
    1.37  
    1.38 -Goal "(D c`(Discr s) = (Def t)) = (<c,s> -c-> t)";
    1.39 +Goal "(D c$(Discr s) = (Def t)) = (<c,s> -c-> t)";
    1.40  by (fast_tac (claset() addSEs [D_implies_eval,eval_implies_D]) 1);
    1.41  qed "D_is_eval";
     2.1 --- a/src/HOLCF/IMP/Denotational.thy	Tue Jan 09 15:32:27 2001 +0100
     2.2 +++ b/src/HOLCF/IMP/Denotational.thy	Tue Jan 09 15:36:30 2001 +0100
     2.3 @@ -10,7 +10,7 @@
     2.4  
     2.5  constdefs
     2.6     dlift :: "(('a::term) discr -> 'b::pcpo) => ('a lift -> 'b)"
     2.7 -  "dlift f == (LAM x. case x of Undef => UU | Def(y) => f`(Discr y))"
     2.8 +  "dlift f == (LAM x. case x of Undef => UU | Def(y) => f$(Discr y))"
     2.9  
    2.10  consts D :: "com => state discr -> state lift"
    2.11  
    2.12 @@ -19,9 +19,9 @@
    2.13    "D(X :== a) = (LAM s. Def((undiscr s)[X ::= a(undiscr s)]))"
    2.14    "D(c0 ; c1) = (dlift(D c1) oo (D c0))"
    2.15    "D(IF b THEN c1 ELSE c2) =
    2.16 -	(LAM s. if b(undiscr s) then (D c1)`s else (D c2)`s)"
    2.17 +	(LAM s. if b(undiscr s) then (D c1)$s else (D c2)$s)"
    2.18    "D(WHILE b DO c) =
    2.19 -	fix`(LAM w s. if b(undiscr s) then (dlift w)`((D c)`s)
    2.20 +	fix$(LAM w s. if b(undiscr s) then (dlift w)$((D c)$s)
    2.21                        else Def(undiscr s))"
    2.22  
    2.23  end
     3.1 --- a/src/HOLCF/IMP/HoareEx.thy	Tue Jan 09 15:32:27 2001 +0100
     3.2 +++ b/src/HOLCF/IMP/HoareEx.thy	Tue Jan 09 15:36:30 2001 +0100
     3.3 @@ -13,6 +13,6 @@
     3.4  types assn = state => bool
     3.5  
     3.6  constdefs hoare_valid :: [assn,com,assn] => bool ("|= {(1_)}/ (_)/ {(1_)}" 50)
     3.7 - "|= {A} c {B} == !s t. A s & D c `(Discr s) = Def t --> B t"
     3.8 + "|= {A} c {B} == !s t. A s & D c $(Discr s) = Def t --> B t"
     3.9  
    3.10  end
     4.1 --- a/src/HOLCF/IOA/meta_theory/Abstraction.ML	Tue Jan 09 15:32:27 2001 +0100
     4.2 +++ b/src/HOLCF/IOA/meta_theory/Abstraction.ML	Tue Jan 09 15:36:30 2001 +0100
     4.3 @@ -181,7 +181,7 @@
     4.4     that is to special Map Lemma *)
     4.5  Goalw [cex_abs_def,mk_trace_def,filter_act_def]
     4.6    "ext C = ext A \
     4.7 -\        ==> mk_trace C`xs = mk_trace A`(snd (cex_abs f (s,xs)))";
     4.8 +\        ==> mk_trace C$xs = mk_trace A$(snd (cex_abs f (s,xs)))";
     4.9  by (Asm_full_simp_tac 1);
    4.10  by (pair_induct_tac "xs" [] 1);
    4.11  qed"traces_coincide_abs";
    4.12 @@ -383,11 +383,11 @@
    4.13  
    4.14  (* FIX: NAch Sequence.ML bringen *)
    4.15  
    4.16 -Goal "(Map f`s = nil) = (s=nil)";
    4.17 +Goal "(Map f$s = nil) = (s=nil)";
    4.18  by (Seq_case_simp_tac "s" 1);
    4.19  qed"Mapnil";
    4.20  
    4.21 -Goal "(Map f`s = UU) = (s=UU)";
    4.22 +Goal "(Map f$s = UU) = (s=UU)";
    4.23  by (Seq_case_simp_tac "s" 1);
    4.24  qed"MapUU";
    4.25  
    4.26 @@ -400,7 +400,7 @@
    4.27  by Auto_tac;
    4.28  by (asm_full_simp_tac (simpset() addsimps [Mapnil])1);
    4.29  by (asm_full_simp_tac (simpset() addsimps [MapUU])1);
    4.30 -by (res_inst_tac [("x","Map (%(s,a,t). (h s,a, h t))`s1")] exI 1);
    4.31 +by (res_inst_tac [("x","Map (%(s,a,t). (h s,a, h t))$s1")] exI 1);
    4.32  by (asm_full_simp_tac (simpset() addsimps [Map2Finite,MapConc])1);
    4.33  qed"cex_absSeq_tsuffix";
    4.34  
    4.35 @@ -433,7 +433,7 @@
    4.36  (* ------------------ Next ----------------------------*)
    4.37  
    4.38  Goal 
    4.39 -"(TL`(ex2seq (cex_abs h ex))=UU) = (TL`(ex2seq ex)=UU)";
    4.40 +"(TL$(ex2seq (cex_abs h ex))=UU) = (TL$(ex2seq ex)=UU)";
    4.41  by (pair_tac "ex" 1);
    4.42  by (Seq_case_simp_tac "y" 1);
    4.43  by (pair_tac "a" 1);
    4.44 @@ -442,7 +442,7 @@
    4.45  qed"TL_ex2seq_UU";
    4.46  
    4.47  Goal 
    4.48 -"(TL`(ex2seq (cex_abs h ex))=nil) = (TL`(ex2seq ex)=nil)";
    4.49 +"(TL$(ex2seq (cex_abs h ex))=nil) = (TL$(ex2seq ex)=nil)";
    4.50  by (pair_tac "ex" 1);
    4.51  by (Seq_case_simp_tac "y" 1);
    4.52  by (pair_tac "a" 1);
    4.53 @@ -451,7 +451,7 @@
    4.54  qed"TL_ex2seq_nil";
    4.55  
    4.56  (* FIX: put to Sequence Lemmas *)
    4.57 -Goal "Map f`(TL`s) = TL`(Map f`s)";
    4.58 +Goal "Map f$(TL$s) = TL$(Map f$s)";
    4.59  by (Seq_induct_tac "s" [] 1);
    4.60  qed"MapTL";
    4.61  
    4.62 @@ -459,13 +459,13 @@
    4.63    properties carry over *)
    4.64  
    4.65  Goalw [cex_absSeq_def]
    4.66 -"cex_absSeq h (TL`s) = (TL`(cex_absSeq h s))";
    4.67 +"cex_absSeq h (TL$s) = (TL$(cex_absSeq h s))";
    4.68  by (simp_tac (simpset() addsimps [MapTL]) 1);
    4.69  qed"cex_absSeq_TL";
    4.70  
    4.71  (* important property of ex2seq: can be shiftet, as defined "pointwise" *)
    4.72  
    4.73 -Goal "[| (snd ex)~=UU ; (snd ex)~=nil |] ==> (? ex'. TL`(ex2seq ex) = ex2seq ex')";
    4.74 +Goal "[| (snd ex)~=UU ; (snd ex)~=nil |] ==> (? ex'. TL$(ex2seq ex) = ex2seq ex')";
    4.75  by (pair_tac "ex" 1);
    4.76  by (Seq_case_simp_tac "y" 1);
    4.77  by (pair_tac "a" 1);
    4.78 @@ -473,7 +473,7 @@
    4.79  qed"TLex2seq";
    4.80  
    4.81   
    4.82 -Goal "(TL`(ex2seq ex)~=nil) = ((snd ex)~=nil & (snd ex)~=UU)";
    4.83 +Goal "(TL$(ex2seq ex)~=nil) = ((snd ex)~=nil & (snd ex)~=UU)";
    4.84  by (pair_tac "ex" 1);
    4.85  by (Seq_case_simp_tac "y" 1);
    4.86  by (pair_tac "a" 1);
     5.1 --- a/src/HOLCF/IOA/meta_theory/Abstraction.thy	Tue Jan 09 15:32:27 2001 +0100
     5.2 +++ b/src/HOLCF/IOA/meta_theory/Abstraction.thy	Tue Jan 09 15:36:30 2001 +0100
     5.3 @@ -43,11 +43,11 @@
     5.4        temp_weakening (snd AM) (snd CL) h"
     5.5  
     5.6  cex_abs_def
     5.7 -  "cex_abs f ex == (f (fst ex), Map (%(a,t). (a,f t))`(snd ex))"
     5.8 +  "cex_abs f ex == (f (fst ex), Map (%(a,t). (a,f t))$(snd ex))"
     5.9  
    5.10  (* equals cex_abs on Sequneces -- after ex2seq application -- *)
    5.11  cex_absSeq_def
    5.12 -  "cex_absSeq f == % s. Map (%(s,a,t). (f s,a,f t))`s"
    5.13 +  "cex_absSeq f == % s. Map (%(s,a,t). (f s,a,f t))$s"
    5.14  
    5.15  weakeningIOA_def
    5.16     "weakeningIOA A C h == ! ex. ex : executions C --> cex_abs h ex : executions A"
     6.1 --- a/src/HOLCF/IOA/meta_theory/CompoExecs.ML	Tue Jan 09 15:32:27 2001 +0100
     6.2 +++ b/src/HOLCF/IOA/meta_theory/CompoExecs.ML	Tue Jan 09 15:36:30 2001 +0100
     6.3 @@ -20,15 +20,15 @@
     6.4  (* ---------------------------------------------------------------- *)
     6.5  
     6.6  
     6.7 -Goal  "ProjA2`UU = UU";
     6.8 +Goal  "ProjA2$UU = UU";
     6.9  by (simp_tac (simpset() addsimps [ProjA2_def]) 1);
    6.10  qed"ProjA2_UU";
    6.11  
    6.12 -Goal  "ProjA2`nil = nil";
    6.13 +Goal  "ProjA2$nil = nil";
    6.14  by (simp_tac (simpset() addsimps [ProjA2_def]) 1);
    6.15  qed"ProjA2_nil";
    6.16  
    6.17 -Goal "ProjA2`((a,t)>>xs) = (a,fst t) >> ProjA2`xs";
    6.18 +Goal "ProjA2$((a,t)>>xs) = (a,fst t) >> ProjA2$xs";
    6.19  by (simp_tac (simpset() addsimps [ProjA2_def]) 1);
    6.20  qed"ProjA2_cons";
    6.21  
    6.22 @@ -38,15 +38,15 @@
    6.23  (* ---------------------------------------------------------------- *)
    6.24  
    6.25  
    6.26 -Goal  "ProjB2`UU = UU";
    6.27 +Goal  "ProjB2$UU = UU";
    6.28  by (simp_tac (simpset() addsimps [ProjB2_def]) 1);
    6.29  qed"ProjB2_UU";
    6.30  
    6.31 -Goal  "ProjB2`nil = nil";
    6.32 +Goal  "ProjB2$nil = nil";
    6.33  by (simp_tac (simpset() addsimps [ProjB2_def]) 1);
    6.34  qed"ProjB2_nil";
    6.35  
    6.36 -Goal "ProjB2`((a,t)>>xs) = (a,snd t) >> ProjB2`xs";
    6.37 +Goal "ProjB2$((a,t)>>xs) = (a,snd t) >> ProjB2$xs";
    6.38  by (simp_tac (simpset() addsimps [ProjB2_def]) 1);
    6.39  qed"ProjB2_cons";
    6.40  
    6.41 @@ -57,18 +57,18 @@
    6.42  (* ---------------------------------------------------------------- *)
    6.43  
    6.44  
    6.45 -Goal "Filter_ex2 sig`UU=UU";
    6.46 +Goal "Filter_ex2 sig$UU=UU";
    6.47  by (simp_tac (simpset() addsimps [Filter_ex2_def]) 1);
    6.48  qed"Filter_ex2_UU";
    6.49  
    6.50 -Goal "Filter_ex2 sig`nil=nil";
    6.51 +Goal "Filter_ex2 sig$nil=nil";
    6.52  by (simp_tac (simpset() addsimps [Filter_ex2_def]) 1);
    6.53  qed"Filter_ex2_nil";
    6.54  
    6.55 -Goal "Filter_ex2 sig`(at >> xs) =    \
    6.56 +Goal "Filter_ex2 sig$(at >> xs) =    \
    6.57  \            (if (fst at:actions sig)    \       
    6.58 -\                 then at >> (Filter_ex2 sig`xs) \   
    6.59 -\                 else        Filter_ex2 sig`xs)";
    6.60 +\                 then at >> (Filter_ex2 sig$xs) \   
    6.61 +\                 else        Filter_ex2 sig$xs)";
    6.62  
    6.63  by (asm_full_simp_tac (simpset() addsimps [Filter_ex2_def]) 1);
    6.64  qed"Filter_ex2_cons";
    6.65 @@ -85,8 +85,8 @@
    6.66  \            (%p.(If Def ((fst p)~:actions sig) \
    6.67  \                 then Def (s=(snd p)) \
    6.68  \                 else TT fi) \
    6.69 -\                andalso (stutter2 sig`xs) (snd p))  \
    6.70 -\             `x) \
    6.71 +\                andalso (stutter2 sig$xs) (snd p))  \
    6.72 +\             $x) \
    6.73  \           ))";
    6.74  by (rtac trans 1);
    6.75  by (rtac fix_eq2 1);
    6.76 @@ -95,19 +95,19 @@
    6.77  by (simp_tac (simpset() addsimps [flift1_def]) 1);
    6.78  qed"stutter2_unfold";
    6.79  
    6.80 -Goal "(stutter2 sig`UU) s=UU";
    6.81 +Goal "(stutter2 sig$UU) s=UU";
    6.82  by (stac stutter2_unfold 1);
    6.83  by (Simp_tac 1);
    6.84  qed"stutter2_UU";
    6.85  
    6.86 -Goal "(stutter2 sig`nil) s = TT";
    6.87 +Goal "(stutter2 sig$nil) s = TT";
    6.88  by (stac stutter2_unfold 1);
    6.89  by (Simp_tac 1);
    6.90  qed"stutter2_nil";
    6.91  
    6.92 -Goal "(stutter2 sig`(at>>xs)) s = \
    6.93 +Goal "(stutter2 sig$(at>>xs)) s = \
    6.94  \              ((if (fst at)~:actions sig then Def (s=snd at) else TT) \
    6.95 -\                andalso (stutter2 sig`xs) (snd at))"; 
    6.96 +\                andalso (stutter2 sig$xs) (snd at))"; 
    6.97  by (rtac trans 1);
    6.98  by (stac stutter2_unfold 1);
    6.99  by (asm_full_simp_tac (simpset() addsimps [Consq_def,flift1_def,If_and_if]) 1);
   6.100 @@ -159,8 +159,8 @@
   6.101  (* --------------------------------------------------------------------- *)
   6.102  
   6.103  Goal "!s. is_exec_frag (A||B) (s,xs) \
   6.104 -\      -->  is_exec_frag A (fst s, Filter_ex2 (asig_of A)`(ProjA2`xs)) &\
   6.105 -\           is_exec_frag B (snd s, Filter_ex2 (asig_of B)`(ProjB2`xs))";
   6.106 +\      -->  is_exec_frag A (fst s, Filter_ex2 (asig_of A)$(ProjA2$xs)) &\
   6.107 +\           is_exec_frag B (snd s, Filter_ex2 (asig_of B)$(ProjB2$xs))";
   6.108  
   6.109  by (pair_induct_tac "xs" [is_exec_frag_def] 1);
   6.110  (* main case *)
   6.111 @@ -175,8 +175,8 @@
   6.112  (* --------------------------------------------------------------------- *)
   6.113  
   6.114  Goal "!s. is_exec_frag (A||B) (s,xs) \
   6.115 -\      --> stutter (asig_of A) (fst s,ProjA2`xs)  &\
   6.116 -\          stutter (asig_of B) (snd s,ProjB2`xs)"; 
   6.117 +\      --> stutter (asig_of A) (fst s,ProjA2$xs)  &\
   6.118 +\          stutter (asig_of B) (snd s,ProjB2$xs)"; 
   6.119  
   6.120  by (pair_induct_tac "xs" [stutter_def,is_exec_frag_def] 1);
   6.121  (* main case *)
   6.122 @@ -205,10 +205,10 @@
   6.123  (* ----------------------------------------------------------------------- *)
   6.124  
   6.125  Goal 
   6.126 -"!s. is_exec_frag A (fst s,Filter_ex2 (asig_of A)`(ProjA2`xs)) &\
   6.127 -\    is_exec_frag B (snd s,Filter_ex2 (asig_of B)`(ProjB2`xs)) &\
   6.128 -\    stutter (asig_of A) (fst s,(ProjA2`xs)) & \
   6.129 -\    stutter (asig_of B) (snd s,(ProjB2`xs)) & \
   6.130 +"!s. is_exec_frag A (fst s,Filter_ex2 (asig_of A)$(ProjA2$xs)) &\
   6.131 +\    is_exec_frag B (snd s,Filter_ex2 (asig_of B)$(ProjB2$xs)) &\
   6.132 +\    stutter (asig_of A) (fst s,(ProjA2$xs)) & \
   6.133 +\    stutter (asig_of B) (snd s,(ProjB2$xs)) & \
   6.134  \    Forall (%x. fst x:act (A||B)) xs \
   6.135  \    --> is_exec_frag (A||B) (s,xs)";
   6.136  
     7.1 --- a/src/HOLCF/IOA/meta_theory/CompoExecs.thy	Tue Jan 09 15:32:27 2001 +0100
     7.2 +++ b/src/HOLCF/IOA/meta_theory/CompoExecs.thy	Tue Jan 09 15:36:30 2001 +0100
     7.3 @@ -27,10 +27,10 @@
     7.4  
     7.5  
     7.6  ProjA_def
     7.7 - "ProjA ex == (fst (fst ex), ProjA2`(snd ex))" 
     7.8 + "ProjA ex == (fst (fst ex), ProjA2$(snd ex))" 
     7.9  
    7.10  ProjB_def
    7.11 - "ProjB ex == (snd (fst ex), ProjB2`(snd ex))" 
    7.12 + "ProjB ex == (snd (fst ex), ProjB2$(snd ex))" 
    7.13  
    7.14  
    7.15  ProjA2_def
    7.16 @@ -41,24 +41,24 @@
    7.17   
    7.18  
    7.19  Filter_ex_def
    7.20 -  "Filter_ex sig ex == (fst ex,Filter_ex2 sig`(snd ex))"
    7.21 +  "Filter_ex sig ex == (fst ex,Filter_ex2 sig$(snd ex))"
    7.22  
    7.23  
    7.24  Filter_ex2_def
    7.25    "Filter_ex2 sig ==  Filter (%x. fst x:actions sig)"
    7.26  
    7.27  stutter_def
    7.28 -  "stutter sig ex == ((stutter2 sig`(snd ex)) (fst ex) ~= FF)"
    7.29 +  "stutter sig ex == ((stutter2 sig$(snd ex)) (fst ex) ~= FF)"
    7.30  
    7.31  stutter2_def
    7.32 -  "stutter2 sig ==(fix`(LAM h ex. (%s. case ex of 
    7.33 +  "stutter2 sig ==(fix$(LAM h ex. (%s. case ex of 
    7.34        nil => TT
    7.35      | x##xs => (flift1 
    7.36              (%p.(If Def ((fst p)~:actions sig)
    7.37                   then Def (s=(snd p)) 
    7.38                   else TT fi)
    7.39 -                andalso (h`xs) (snd p)) 
    7.40 -             `x)
    7.41 +                andalso (h$xs) (snd p)) 
    7.42 +             $x)
    7.43     )))" 
    7.44  
    7.45  par_execs_def
     8.1 --- a/src/HOLCF/IOA/meta_theory/CompoScheds.ML	Tue Jan 09 15:32:27 2001 +0100
     8.2 +++ b/src/HOLCF/IOA/meta_theory/CompoScheds.ML	Tue Jan 09 15:36:30 2001 +0100
     8.3 @@ -30,25 +30,25 @@
     8.4  \     | Def y =>  \
     8.5  \        (if y:act A then \
     8.6  \            (if y:act B then \
     8.7 -\               (case HD`exA of \
     8.8 +\               (case HD$exA of \
     8.9  \                  Undef => UU \
    8.10 -\                | Def a => (case HD`exB of \
    8.11 +\                | Def a => (case HD$exB of \
    8.12  \                             Undef => UU \
    8.13  \                           | Def b => \
    8.14  \                  (y,(snd a,snd b))>>  \
    8.15 -\                    (mkex2 A B`xs`(TL`exA)`(TL`exB)) (snd a) (snd b)))  \
    8.16 +\                    (mkex2 A B$xs$(TL$exA)$(TL$exB)) (snd a) (snd b)))  \
    8.17  \             else   \
    8.18 -\               (case HD`exA of   \
    8.19 +\               (case HD$exA of   \
    8.20  \                  Undef => UU  \
    8.21  \                | Def a => \
    8.22 -\                  (y,(snd a,t))>>(mkex2 A B`xs`(TL`exA)`exB) (snd a) t)  \
    8.23 +\                  (y,(snd a,t))>>(mkex2 A B$xs$(TL$exA)$exB) (snd a) t)  \
    8.24  \             )  \       
    8.25  \         else   \
    8.26  \            (if y:act B then \
    8.27 -\               (case HD`exB of  \
    8.28 +\               (case HD$exB of  \
    8.29  \                  Undef => UU  \
    8.30  \                | Def b =>  \
    8.31 -\                  (y,(s,snd b))>>(mkex2 A B`xs`exA`(TL`exB)) s (snd b))  \
    8.32 +\                  (y,(s,snd b))>>(mkex2 A B$xs$exA$(TL$exB)) s (snd b))  \
    8.33  \            else  \
    8.34  \              UU  \
    8.35  \            )  \
    8.36 @@ -56,38 +56,38 @@
    8.37  \      )))");
    8.38  
    8.39  
    8.40 -Goal "(mkex2 A B`UU`exA`exB) s t = UU";
    8.41 +Goal "(mkex2 A B$UU$exA$exB) s t = UU";
    8.42  by (stac mkex2_unfold 1);
    8.43  by (Simp_tac 1);
    8.44  qed"mkex2_UU";
    8.45  
    8.46 -Goal "(mkex2 A B`nil`exA`exB) s t= nil";
    8.47 +Goal "(mkex2 A B$nil$exA$exB) s t= nil";
    8.48  by (stac mkex2_unfold 1);
    8.49  by (Simp_tac 1);
    8.50  qed"mkex2_nil";
    8.51  
    8.52 -Goal "[| x:act A; x~:act B; HD`exA=Def a|] \
    8.53 -\   ==> (mkex2 A B`(x>>sch)`exA`exB) s t =   \
    8.54 -\       (x,snd a,t) >> (mkex2 A B`sch`(TL`exA)`exB) (snd a) t";
    8.55 +Goal "[| x:act A; x~:act B; HD$exA=Def a|] \
    8.56 +\   ==> (mkex2 A B$(x>>sch)$exA$exB) s t =   \
    8.57 +\       (x,snd a,t) >> (mkex2 A B$sch$(TL$exA)$exB) (snd a) t";
    8.58  by (rtac trans 1);
    8.59  by (stac mkex2_unfold 1);
    8.60  by (asm_full_simp_tac (simpset() addsimps [Consq_def,If_and_if]) 1);
    8.61  by (asm_full_simp_tac (simpset() addsimps [Consq_def]) 1);
    8.62  qed"mkex2_cons_1";
    8.63  
    8.64 -Goal "[| x~:act A; x:act B; HD`exB=Def b|] \
    8.65 -\   ==> (mkex2 A B`(x>>sch)`exA`exB) s t = \
    8.66 -\       (x,s,snd b) >> (mkex2 A B`sch`exA`(TL`exB)) s (snd b)";
    8.67 +Goal "[| x~:act A; x:act B; HD$exB=Def b|] \
    8.68 +\   ==> (mkex2 A B$(x>>sch)$exA$exB) s t = \
    8.69 +\       (x,s,snd b) >> (mkex2 A B$sch$exA$(TL$exB)) s (snd b)";
    8.70  by (rtac trans 1);
    8.71  by (stac mkex2_unfold 1);
    8.72  by (asm_full_simp_tac (simpset() addsimps [Consq_def,If_and_if]) 1);
    8.73  by (asm_full_simp_tac (simpset() addsimps [Consq_def]) 1);
    8.74  qed"mkex2_cons_2";
    8.75  
    8.76 -Goal "[| x:act A; x:act B; HD`exA=Def a;HD`exB=Def b|] \
    8.77 -\   ==> (mkex2 A B`(x>>sch)`exA`exB) s t =  \
    8.78 +Goal "[| x:act A; x:act B; HD$exA=Def a;HD$exB=Def b|] \
    8.79 +\   ==> (mkex2 A B$(x>>sch)$exA$exB) s t =  \
    8.80  \        (x,snd a,snd b) >> \
    8.81 -\           (mkex2 A B`sch`(TL`exA)`(TL`exB)) (snd a) (snd b)";
    8.82 +\           (mkex2 A B$sch$(TL$exA)$(TL$exB)) (snd a) (snd b)";
    8.83  by (rtac trans 1);
    8.84  by (stac mkex2_unfold 1);
    8.85  by (asm_full_simp_tac (simpset() addsimps [Consq_def,If_and_if]) 1);
    8.86 @@ -156,8 +156,8 @@
    8.87  (* --------------------------------------------------------------------- *)
    8.88  
    8.89  Goalw [filter_act_def,Filter_ex2_def]
    8.90 -   "filter_act`(Filter_ex2 (asig_of A)`xs)=\
    8.91 -\   Filter (%a. a:act A)`(filter_act`xs)";
    8.92 +   "filter_act$(Filter_ex2 (asig_of A)$xs)=\
    8.93 +\   Filter (%a. a:act A)$(filter_act$xs)";
    8.94  
    8.95  by (simp_tac (simpset() addsimps [MapFilter,o_def]) 1);
    8.96  qed"lemma_2_1a";
    8.97 @@ -168,8 +168,8 @@
    8.98  (* --------------------------------------------------------------------- *)
    8.99  
   8.100  Goal 
   8.101 -   "filter_act`(ProjA2`xs) =filter_act`xs &\
   8.102 -\   filter_act`(ProjB2`xs) =filter_act`xs";
   8.103 +   "filter_act$(ProjA2$xs) =filter_act$xs &\
   8.104 +\   filter_act$(ProjB2$xs) =filter_act$xs";
   8.105  
   8.106  by (pair_induct_tac "xs" [] 1);
   8.107  qed"lemma_2_1b";
   8.108 @@ -184,7 +184,7 @@
   8.109     is the same proposition, but we cannot change this one, when then rather lemma_1_1c  *)
   8.110  
   8.111  Goal "!s. is_exec_frag (A||B) (s,xs) \
   8.112 -\  --> Forall (%x. x:act (A||B)) (filter_act`xs)";
   8.113 +\  --> Forall (%x. x:act (A||B)) (filter_act$xs)";
   8.114  
   8.115  by (pair_induct_tac "xs" [is_exec_frag_def,Forall_def,sforall_def] 1);
   8.116  (* main case *)
   8.117 @@ -205,9 +205,9 @@
   8.118  
   8.119  Goal "! exA exB s t. \
   8.120  \ Forall (%x. x:act (A||B)) sch  & \
   8.121 -\ Filter (%a. a:act A)`sch << filter_act`exA &\
   8.122 -\ Filter (%a. a:act B)`sch << filter_act`exB \
   8.123 -\ --> filter_act`(snd (mkex A B sch (s,exA) (t,exB))) = sch";
   8.124 +\ Filter (%a. a:act A)$sch << filter_act$exA &\
   8.125 +\ Filter (%a. a:act B)$sch << filter_act$exB \
   8.126 +\ --> filter_act$(snd (mkex A B sch (s,exA) (t,exB))) = sch";
   8.127  
   8.128  by (Seq_induct_tac "sch" [Filter_def,Forall_def,sforall_def,mkex_def] 1);
   8.129  
   8.130 @@ -268,9 +268,9 @@
   8.131  
   8.132  Goal "! exA exB s t. \
   8.133  \ Forall (%x. x:act (A||B)) sch & \
   8.134 -\ Filter (%a. a:act A)`sch << filter_act`exA &\
   8.135 -\ Filter (%a. a:act B)`sch << filter_act`exB \
   8.136 -\ --> stutter (asig_of A) (s,ProjA2`(snd (mkex A B sch (s,exA) (t,exB))))";
   8.137 +\ Filter (%a. a:act A)$sch << filter_act$exA &\
   8.138 +\ Filter (%a. a:act B)$sch << filter_act$exB \
   8.139 +\ --> stutter (asig_of A) (s,ProjA2$(snd (mkex A B sch (s,exA) (t,exB))))";
   8.140  
   8.141  by (mkex_induct_tac "sch" "exA" "exB");
   8.142  
   8.143 @@ -279,8 +279,8 @@
   8.144  
   8.145  Goal "[|  \
   8.146  \ Forall (%x. x:act (A||B)) sch ; \
   8.147 -\ Filter (%a. a:act A)`sch << filter_act`(snd exA) ;\
   8.148 -\ Filter (%a. a:act B)`sch << filter_act`(snd exB) |] \
   8.149 +\ Filter (%a. a:act A)$sch << filter_act$(snd exA) ;\
   8.150 +\ Filter (%a. a:act B)$sch << filter_act$(snd exB) |] \
   8.151  \ ==> stutter (asig_of A) (ProjA (mkex A B sch exA exB))";
   8.152  
   8.153  by (cut_facts_tac [stutterA_mkex] 1);
   8.154 @@ -299,9 +299,9 @@
   8.155  
   8.156  Goal "! exA exB s t. \
   8.157  \ Forall (%x. x:act (A||B)) sch & \
   8.158 -\ Filter (%a. a:act A)`sch << filter_act`exA &\
   8.159 -\ Filter (%a. a:act B)`sch << filter_act`exB \
   8.160 -\ --> stutter (asig_of B) (t,ProjB2`(snd (mkex A B sch (s,exA) (t,exB))))";
   8.161 +\ Filter (%a. a:act A)$sch << filter_act$exA &\
   8.162 +\ Filter (%a. a:act B)$sch << filter_act$exB \
   8.163 +\ --> stutter (asig_of B) (t,ProjB2$(snd (mkex A B sch (s,exA) (t,exB))))";
   8.164  
   8.165  by (mkex_induct_tac "sch" "exA" "exB");
   8.166  
   8.167 @@ -310,8 +310,8 @@
   8.168  
   8.169  Goal "[|  \
   8.170  \ Forall (%x. x:act (A||B)) sch ; \
   8.171 -\ Filter (%a. a:act A)`sch << filter_act`(snd exA) ;\
   8.172 -\ Filter (%a. a:act B)`sch << filter_act`(snd exB) |] \
   8.173 +\ Filter (%a. a:act A)$sch << filter_act$(snd exA) ;\
   8.174 +\ Filter (%a. a:act B)$sch << filter_act$(snd exB) |] \
   8.175  \ ==> stutter (asig_of B) (ProjB (mkex A B sch exA exB))";
   8.176  
   8.177  by (cut_facts_tac [stutterB_mkex] 1);
   8.178 @@ -325,40 +325,40 @@
   8.179  
   8.180  (*---------------------------------------------------------------------------
   8.181       Filter of mkex(sch,exA,exB) to A after projection onto A is exA 
   8.182 -        --  using zip`(proj1`exA)`(proj2`exA) instead of exA    --
   8.183 +        --  using zip$(proj1$exA)$(proj2$exA) instead of exA    --
   8.184          --           because of admissibility problems          --
   8.185                               structural induction
   8.186    --------------------------------------------------------------------------- *)
   8.187  
   8.188  Goal "! exA exB s t. \
   8.189  \ Forall (%x. x:act (A||B)) sch & \
   8.190 -\ Filter (%a. a:act A)`sch << filter_act`exA  &\
   8.191 -\ Filter (%a. a:act B)`sch << filter_act`exB \
   8.192 -\ --> Filter_ex2 (asig_of A)`(ProjA2`(snd (mkex A B sch (s,exA) (t,exB)))) =   \
   8.193 -\     Zip`(Filter (%a. a:act A)`sch)`(Map snd`exA)";
   8.194 +\ Filter (%a. a:act A)$sch << filter_act$exA  &\
   8.195 +\ Filter (%a. a:act B)$sch << filter_act$exB \
   8.196 +\ --> Filter_ex2 (asig_of A)$(ProjA2$(snd (mkex A B sch (s,exA) (t,exB)))) =   \
   8.197 +\     Zip$(Filter (%a. a:act A)$sch)$(Map snd$exA)";
   8.198  
   8.199  by (mkex_induct_tac "sch" "exB" "exA");
   8.200  
   8.201  qed"filter_mkex_is_exA_tmp";
   8.202  
   8.203  (*---------------------------------------------------------------------------
   8.204 -                      zip`(proj1`y)`(proj2`y) = y   (using the lift operations)
   8.205 +                      zip$(proj1$y)$(proj2$y) = y   (using the lift operations)
   8.206                      lemma for admissibility problems         
   8.207    --------------------------------------------------------------------------- *)
   8.208  
   8.209 -Goal  "Zip`(Map fst`y)`(Map snd`y) = y";
   8.210 +Goal  "Zip$(Map fst$y)$(Map snd$y) = y";
   8.211  by (Seq_induct_tac "y" [] 1);
   8.212  qed"Zip_Map_fst_snd";
   8.213  
   8.214  
   8.215  (*---------------------------------------------------------------------------
   8.216 -      filter A`sch = proj1`ex   -->  zip`(filter A`sch)`(proj2`ex) = ex 
   8.217 +      filter A$sch = proj1$ex   -->  zip$(filter A$sch)$(proj2$ex) = ex 
   8.218           lemma for eliminating non admissible equations in assumptions      
   8.219    --------------------------------------------------------------------------- *)
   8.220  
   8.221  Goal "!! sch ex. \
   8.222 -\ Filter (%a. a:act AB)`sch = filter_act`ex  \
   8.223 -\ ==> ex = Zip`(Filter (%a. a:act AB)`sch)`(Map snd`ex)";
   8.224 +\ Filter (%a. a:act AB)$sch = filter_act$ex  \
   8.225 +\ ==> ex = Zip$(Filter (%a. a:act AB)$sch)$(Map snd$ex)";
   8.226  by (asm_full_simp_tac (simpset() addsimps [filter_act_def]) 1);
   8.227  by (rtac (Zip_Map_fst_snd RS sym) 1);
   8.228  qed"trick_against_eq_in_ass";
   8.229 @@ -371,8 +371,8 @@
   8.230  
   8.231  Goal "!!sch exA exB.\
   8.232  \ [| Forall (%a. a:act (A||B)) sch ; \
   8.233 -\ Filter (%a. a:act A)`sch = filter_act`(snd exA)  ;\
   8.234 -\ Filter (%a. a:act B)`sch = filter_act`(snd exB) |]\
   8.235 +\ Filter (%a. a:act A)$sch = filter_act$(snd exA)  ;\
   8.236 +\ Filter (%a. a:act B)$sch = filter_act$(snd exB) |]\
   8.237  \ ==> Filter_ex (asig_of A) (ProjA (mkex A B sch exA exB)) = exA";
   8.238  by (asm_full_simp_tac (simpset() addsimps [ProjA_def,Filter_ex_def]) 1);
   8.239  by (pair_tac "exA" 1);
   8.240 @@ -388,7 +388,7 @@
   8.241  
   8.242  (*---------------------------------------------------------------------------
   8.243       Filter of mkex(sch,exA,exB) to B after projection onto B is exB 
   8.244 -        --  using zip`(proj1`exB)`(proj2`exB) instead of exB    --
   8.245 +        --  using zip$(proj1$exB)$(proj2$exB) instead of exB    --
   8.246          --           because of admissibility problems          --
   8.247                               structural induction
   8.248    --------------------------------------------------------------------------- *)
   8.249 @@ -396,10 +396,10 @@
   8.250  
   8.251  Goal "! exA exB s t. \
   8.252  \ Forall (%x. x:act (A||B)) sch & \
   8.253 -\ Filter (%a. a:act A)`sch << filter_act`exA  &\
   8.254 -\ Filter (%a. a:act B)`sch << filter_act`exB \
   8.255 -\ --> Filter_ex2 (asig_of B)`(ProjB2`(snd (mkex A B sch (s,exA) (t,exB)))) =   \
   8.256 -\     Zip`(Filter (%a. a:act B)`sch)`(Map snd`exB)";
   8.257 +\ Filter (%a. a:act A)$sch << filter_act$exA  &\
   8.258 +\ Filter (%a. a:act B)$sch << filter_act$exB \
   8.259 +\ --> Filter_ex2 (asig_of B)$(ProjB2$(snd (mkex A B sch (s,exA) (t,exB)))) =   \
   8.260 +\     Zip$(Filter (%a. a:act B)$sch)$(Map snd$exB)";
   8.261  
   8.262  (* notice necessary change of arguments exA and exB *)
   8.263  by (mkex_induct_tac "sch" "exA" "exB");
   8.264 @@ -415,8 +415,8 @@
   8.265  
   8.266  Goal "!!sch exA exB.\
   8.267  \ [| Forall (%a. a:act (A||B)) sch ; \
   8.268 -\ Filter (%a. a:act A)`sch = filter_act`(snd exA)  ;\
   8.269 -\ Filter (%a. a:act B)`sch = filter_act`(snd exB) |]\
   8.270 +\ Filter (%a. a:act A)$sch = filter_act$(snd exA)  ;\
   8.271 +\ Filter (%a. a:act B)$sch = filter_act$(snd exB) |]\
   8.272  \ ==> Filter_ex (asig_of B) (ProjB (mkex A B sch exA exB)) = exB";
   8.273  by (asm_full_simp_tac (simpset() addsimps [ProjB_def,Filter_ex_def]) 1);
   8.274  by (pair_tac "exA" 1);
   8.275 @@ -436,8 +436,8 @@
   8.276  
   8.277  Goal "!s t exA exB. \
   8.278  \ Forall (%x. x : act (A || B)) sch &\
   8.279 -\ Filter (%a. a:act A)`sch << filter_act`exA  &\
   8.280 -\ Filter (%a. a:act B)`sch << filter_act`exB \
   8.281 +\ Filter (%a. a:act A)$sch << filter_act$exA  &\
   8.282 +\ Filter (%a. a:act B)$sch << filter_act$exB \
   8.283  \  --> Forall (%x. fst x : act (A ||B))   \
   8.284  \        (snd (mkex A B sch (s,exA) (t,exB)))";
   8.285  
   8.286 @@ -453,8 +453,8 @@
   8.287  
   8.288  Goal  
   8.289  "sch : schedules (A||B) = \
   8.290 -\ (Filter (%a. a:act A)`sch : schedules A &\
   8.291 -\  Filter (%a. a:act B)`sch : schedules B &\
   8.292 +\ (Filter (%a. a:act A)$sch : schedules A &\
   8.293 +\  Filter (%a. a:act B)$sch : schedules B &\
   8.294  \  Forall (%x. x:act (A||B)) sch)";
   8.295  
   8.296  by (simp_tac (simpset() addsimps [schedules_def, has_schedule_def]) 1);
     9.1 --- a/src/HOLCF/IOA/meta_theory/CompoScheds.thy	Tue Jan 09 15:32:27 2001 +0100
     9.2 +++ b/src/HOLCF/IOA/meta_theory/CompoScheds.thy	Tue Jan 09 15:36:30 2001 +0100
     9.3 @@ -26,10 +26,10 @@
     9.4  mkex_def  
     9.5    "mkex A B sch exA exB == 
     9.6         ((fst exA,fst exB),
     9.7 -        (mkex2 A B`sch`(snd exA)`(snd exB)) (fst exA) (fst exB))"
     9.8 +        (mkex2 A B$sch$(snd exA)$(snd exB)) (fst exA) (fst exB))"
     9.9  
    9.10  mkex2_def
    9.11 -  "mkex2 A B == (fix`(LAM h sch exA exB. (%s t. case sch of 
    9.12 +  "mkex2 A B == (fix$(LAM h sch exA exB. (%s t. case sch of 
    9.13         nil => nil
    9.14      | x##xs => 
    9.15        (case x of 
    9.16 @@ -37,25 +37,25 @@
    9.17        | Def y => 
    9.18           (if y:act A then 
    9.19               (if y:act B then 
    9.20 -                (case HD`exA of
    9.21 +                (case HD$exA of
    9.22                     Undef => UU
    9.23 -                 | Def a => (case HD`exB of
    9.24 +                 | Def a => (case HD$exB of
    9.25                                Undef => UU
    9.26                              | Def b => 
    9.27                     (y,(snd a,snd b))>>
    9.28 -                     (h`xs`(TL`exA)`(TL`exB)) (snd a) (snd b)))
    9.29 +                     (h$xs$(TL$exA)$(TL$exB)) (snd a) (snd b)))
    9.30                else
    9.31 -                (case HD`exA of
    9.32 +                (case HD$exA of
    9.33                     Undef => UU
    9.34                   | Def a => 
    9.35 -                   (y,(snd a,t))>>(h`xs`(TL`exA)`exB) (snd a) t)
    9.36 +                   (y,(snd a,t))>>(h$xs$(TL$exA)$exB) (snd a) t)
    9.37                )
    9.38            else 
    9.39               (if y:act B then 
    9.40 -                (case HD`exB of
    9.41 +                (case HD$exB of
    9.42                     Undef => UU
    9.43                   | Def b => 
    9.44 -                   (y,(s,snd b))>>(h`xs`exA`(TL`exB)) s (snd b))
    9.45 +                   (y,(s,snd b))>>(h$xs$exA$(TL$exB)) s (snd b))
    9.46               else
    9.47                 UU
    9.48               )
    9.49 @@ -67,8 +67,8 @@
    9.50         let schA = fst SchedsA; sigA = snd SchedsA; 
    9.51             schB = fst SchedsB; sigB = snd SchedsB       
    9.52         in
    9.53 -       (    {sch. Filter (%a. a:actions sigA)`sch : schA}
    9.54 -        Int {sch. Filter (%a. a:actions sigB)`sch : schB}
    9.55 +       (    {sch. Filter (%a. a:actions sigA)$sch : schA}
    9.56 +        Int {sch. Filter (%a. a:actions sigB)$sch : schB}
    9.57          Int {sch. Forall (%x. x:(actions sigA Un actions sigB)) sch},
    9.58          asig_comp sigA sigB)"
    9.59  
    10.1 --- a/src/HOLCF/IOA/meta_theory/CompoTraces.ML	Tue Jan 09 15:32:27 2001 +0100
    10.2 +++ b/src/HOLCF/IOA/meta_theory/CompoTraces.ML	Tue Jan 09 15:36:30 2001 +0100
    10.3 @@ -24,24 +24,24 @@
    10.4  \      | Def y => \
    10.5  \         (if y:act A then \
    10.6  \             (if y:act B then \ 
    10.7 -\                   ((Takewhile (%a. a:int A)`schA) \
    10.8 -\                         @@(Takewhile (%a. a:int B)`schB) \
    10.9 -\                              @@(y>>(mksch A B`xs   \
   10.10 -\                                       `(TL`(Dropwhile (%a. a:int A)`schA))  \
   10.11 -\                                       `(TL`(Dropwhile (%a. a:int B)`schB))  \
   10.12 +\                   ((Takewhile (%a. a:int A)$schA) \
   10.13 +\                         @@(Takewhile (%a. a:int B)$schB) \
   10.14 +\                              @@(y>>(mksch A B$xs   \
   10.15 +\                                       $(TL$(Dropwhile (%a. a:int A)$schA))  \
   10.16 +\                                       $(TL$(Dropwhile (%a. a:int B)$schB))  \
   10.17  \                    )))   \
   10.18  \              else  \
   10.19 -\                 ((Takewhile (%a. a:int A)`schA)  \
   10.20 -\                      @@ (y>>(mksch A B`xs  \
   10.21 -\                              `(TL`(Dropwhile (%a. a:int A)`schA))  \
   10.22 -\                              `schB)))  \
   10.23 +\                 ((Takewhile (%a. a:int A)$schA)  \
   10.24 +\                      @@ (y>>(mksch A B$xs  \
   10.25 +\                              $(TL$(Dropwhile (%a. a:int A)$schA))  \
   10.26 +\                              $schB)))  \
   10.27  \              )   \
   10.28  \          else    \
   10.29  \             (if y:act B then  \ 
   10.30 -\                 ((Takewhile (%a. a:int B)`schB)  \
   10.31 -\                       @@ (y>>(mksch A B`xs   \
   10.32 -\                              `schA   \
   10.33 -\                              `(TL`(Dropwhile (%a. a:int B)`schB))  \
   10.34 +\                 ((Takewhile (%a. a:int B)$schB)  \
   10.35 +\                       @@ (y>>(mksch A B$xs   \
   10.36 +\                              $schA   \
   10.37 +\                              $(TL$(Dropwhile (%a. a:int B)$schB))  \
   10.38  \                              )))  \
   10.39  \             else  \
   10.40  \               UU  \
   10.41 @@ -50,21 +50,21 @@
   10.42  \       ))");
   10.43  
   10.44  
   10.45 -Goal "mksch A B`UU`schA`schB = UU";
   10.46 +Goal "mksch A B$UU$schA$schB = UU";
   10.47  by (stac mksch_unfold 1);
   10.48  by (Simp_tac 1);
   10.49  qed"mksch_UU";
   10.50  
   10.51 -Goal "mksch A B`nil`schA`schB = nil";
   10.52 +Goal "mksch A B$nil$schA$schB = nil";
   10.53  by (stac mksch_unfold 1);
   10.54  by (Simp_tac 1);
   10.55  qed"mksch_nil";
   10.56  
   10.57  Goal "[|x:act A;x~:act B|]  \
   10.58 -\   ==> mksch A B`(x>>tr)`schA`schB = \
   10.59 -\         (Takewhile (%a. a:int A)`schA) \
   10.60 -\         @@ (x>>(mksch A B`tr`(TL`(Dropwhile (%a. a:int A)`schA)) \
   10.61 -\                             `schB))";
   10.62 +\   ==> mksch A B$(x>>tr)$schA$schB = \
   10.63 +\         (Takewhile (%a. a:int A)$schA) \
   10.64 +\         @@ (x>>(mksch A B$tr$(TL$(Dropwhile (%a. a:int A)$schA)) \
   10.65 +\                             $schB))";
   10.66  by (rtac trans 1);
   10.67  by (stac mksch_unfold 1);
   10.68  by (asm_full_simp_tac (simpset() addsimps [Consq_def,If_and_if]) 1);
   10.69 @@ -72,9 +72,9 @@
   10.70  qed"mksch_cons1";
   10.71  
   10.72  Goal "[|x~:act A;x:act B|] \
   10.73 -\   ==> mksch A B`(x>>tr)`schA`schB = \
   10.74 -\        (Takewhile (%a. a:int B)`schB)  \
   10.75 -\         @@ (x>>(mksch A B`tr`schA`(TL`(Dropwhile (%a. a:int B)`schB))  \
   10.76 +\   ==> mksch A B$(x>>tr)$schA$schB = \
   10.77 +\        (Takewhile (%a. a:int B)$schB)  \
   10.78 +\         @@ (x>>(mksch A B$tr$schA$(TL$(Dropwhile (%a. a:int B)$schB))  \
   10.79  \                            ))";
   10.80  by (rtac trans 1);
   10.81  by (stac mksch_unfold 1);
   10.82 @@ -83,11 +83,11 @@
   10.83  qed"mksch_cons2";
   10.84  
   10.85  Goal "[|x:act A;x:act B|] \
   10.86 -\   ==> mksch A B`(x>>tr)`schA`schB = \
   10.87 -\            (Takewhile (%a. a:int A)`schA) \
   10.88 -\         @@ ((Takewhile (%a. a:int B)`schB)  \
   10.89 -\         @@ (x>>(mksch A B`tr`(TL`(Dropwhile (%a. a:int A)`schA)) \
   10.90 -\                            `(TL`(Dropwhile (%a. a:int B)`schB))))  \
   10.91 +\   ==> mksch A B$(x>>tr)$schA$schB = \
   10.92 +\            (Takewhile (%a. a:int A)$schA) \
   10.93 +\         @@ ((Takewhile (%a. a:int B)$schB)  \
   10.94 +\         @@ (x>>(mksch A B$tr$(TL$(Dropwhile (%a. a:int A)$schA)) \
   10.95 +\                            $(TL$(Dropwhile (%a. a:int B)$schB))))  \
   10.96  \             )";
   10.97  by (rtac trans 1);
   10.98  by (stac mksch_unfold 1);
   10.99 @@ -148,7 +148,7 @@
  10.100  
  10.101  Goal "!!A B. compatible A B ==> \
  10.102  \   ! schA schB. Forall (%x. x:act (A||B)) tr \
  10.103 -\   --> Forall (%x. x:act (A||B)) (mksch A B`tr`schA`schB)";
  10.104 +\   --> Forall (%x. x:act (A||B)) (mksch A B$tr$schA$schB)";
  10.105  by (Seq_induct_tac "tr" [Forall_def,sforall_def,mksch_def] 1); 
  10.106  by (safe_tac set_cs);
  10.107  by (asm_full_simp_tac (simpset() addsimps [actions_of_par]) 1);
  10.108 @@ -175,7 +175,7 @@
  10.109  
  10.110  Goal "!!A B. compatible B A  ==> \
  10.111  \   ! schA schB.  (Forall (%x. x:act B & x~:act A) tr \
  10.112 -\   --> Forall (%x. x:act B & x~:act A) (mksch A B`tr`schA`schB))";
  10.113 +\   --> Forall (%x. x:act B & x~:act A) (mksch A B$tr$schA$schB))";
  10.114  
  10.115  by (Seq_induct_tac "tr" [Forall_def,sforall_def,mksch_def] 1);
  10.116  by (safe_tac set_cs);
  10.117 @@ -186,7 +186,7 @@
  10.118  
  10.119  Goal "!!A B. compatible A B ==> \
  10.120  \   ! schA schB.  (Forall (%x. x:act A & x~:act B) tr \
  10.121 -\   --> Forall (%x. x:act A & x~:act B) (mksch A B`tr`schA`schB))";
  10.122 +\   --> Forall (%x. x:act A & x~:act B) (mksch A B$tr$schA$schB))";
  10.123  
  10.124  by (Seq_induct_tac "tr" [Forall_def,sforall_def,mksch_def] 1);
  10.125  by (safe_tac set_cs);
  10.126 @@ -201,10 +201,10 @@
  10.127  
  10.128  Goal "[| Finite tr; is_asig(asig_of A); is_asig(asig_of B) |] ==> \
  10.129  \   ! x y. Forall (%x. x:act A) x & Forall (%x. x:act B) y & \
  10.130 -\          Filter (%a. a:ext A)`x = Filter (%a. a:act A)`tr & \
  10.131 -\          Filter (%a. a:ext B)`y = Filter (%a. a:act B)`tr &\
  10.132 +\          Filter (%a. a:ext A)$x = Filter (%a. a:act A)$tr & \
  10.133 +\          Filter (%a. a:ext B)$y = Filter (%a. a:act B)$tr &\
  10.134  \          Forall (%x. x:ext (A||B)) tr \
  10.135 -\          --> Finite (mksch A B`tr`x`y)";
  10.136 +\          --> Finite (mksch A B$tr$x$y)";
  10.137  
  10.138  by (etac Seq_Finite_ind  1);
  10.139  by (Asm_full_simp_tac 1);
  10.140 @@ -222,10 +222,10 @@
  10.141            [not_ext_is_int_or_not_act,FiniteConc]) 1);
  10.142  (* now for conclusion IH applicable, but assumptions have to be transformed *)
  10.143  by (dres_inst_tac [("x","x"),
  10.144 -                   ("g","Filter (%a. a:act A)`s")] subst_lemma2 1);
  10.145 +                   ("g","Filter (%a. a:act A)$s")] subst_lemma2 1);
  10.146  by (assume_tac 1);
  10.147  by (dres_inst_tac [("x","y"),
  10.148 -                   ("g","Filter (%a. a:act B)`s")] subst_lemma2 1);
  10.149 +                   ("g","Filter (%a. a:act B)$s")] subst_lemma2 1);
  10.150  by (assume_tac 1);
  10.151  (* IH *)
  10.152  by (asm_full_simp_tac (simpset()
  10.153 @@ -240,7 +240,7 @@
  10.154            [not_ext_is_int_or_not_act,FiniteConc]) 1);
  10.155  (* now for conclusion IH applicable, but assumptions have to be transformed *)
  10.156  by (dres_inst_tac [("x","y"),
  10.157 -                   ("g","Filter (%a. a:act B)`s")] subst_lemma2 1);
  10.158 +                   ("g","Filter (%a. a:act B)$s")] subst_lemma2 1);
  10.159  by (assume_tac 1);
  10.160  (* IH *)
  10.161  by (asm_full_simp_tac (simpset()
  10.162 @@ -255,7 +255,7 @@
  10.163            [not_ext_is_int_or_not_act,FiniteConc]) 1);
  10.164  (* now for conclusion IH applicable, but assumptions have to be transformed *)
  10.165  by (dres_inst_tac [("x","x"),
  10.166 -                   ("g","Filter (%a. a:act A)`s")] subst_lemma2 1);
  10.167 +                   ("g","Filter (%a. a:act A)$s")] subst_lemma2 1);
  10.168  by (assume_tac 1);
  10.169  (* IH *)
  10.170  by (asm_full_simp_tac (simpset()
  10.171 @@ -274,11 +274,11 @@
  10.172  
  10.173  Goal " [| Finite bs; is_asig(asig_of A); is_asig(asig_of B);compatible A B|] ==>  \
  10.174  \! y. Forall (%x. x:act B) y & Forall (%x. x:act B & x~:act A) bs &\
  10.175 -\    Filter (%a. a:ext B)`y = Filter (%a. a:act B)`(bs @@ z) \
  10.176 -\    --> (? y1 y2.  (mksch A B`(bs @@ z)`x`y) = (y1 @@ (mksch A B`z`x`y2)) & \
  10.177 +\    Filter (%a. a:ext B)$y = Filter (%a. a:act B)$(bs @@ z) \
  10.178 +\    --> (? y1 y2.  (mksch A B$(bs @@ z)$x$y) = (y1 @@ (mksch A B$z$x$y2)) & \
  10.179  \                   Forall (%x. x:act B & x~:act A) y1 & \
  10.180  \                   Finite y1 & y = (y1 @@ y2) & \
  10.181 -\                   Filter (%a. a:ext B)`y1 = bs)";
  10.182 +\                   Filter (%a. a:ext B)$y1 = bs)";
  10.183  by (forw_inst_tac [("A1","A")] (compat_commute RS iffD1) 1);
  10.184  by (etac Seq_Finite_ind  1);
  10.185  by (REPEAT (rtac allI 1));
  10.186 @@ -297,12 +297,12 @@
  10.187  by (REPEAT (etac conjE 1));
  10.188  (* transform assumption f eB y = f B (s@z) *)
  10.189  by (dres_inst_tac [("x","y"),
  10.190 -                   ("g","Filter (%a. a:act B)`(s@@z)")] subst_lemma2 1);
  10.191 +                   ("g","Filter (%a. a:act B)$(s@@z)")] subst_lemma2 1);
  10.192  by (assume_tac 1);
  10.193  Addsimps [FilterConc]; 
  10.194  by (asm_full_simp_tac (simpset() addsimps [not_ext_is_int_or_not_act]) 1);
  10.195  (* apply IH *)
  10.196 -by (eres_inst_tac [("x","TL`(Dropwhile (%a. a:int B)`y)")] allE 1);
  10.197 +by (eres_inst_tac [("x","TL$(Dropwhile (%a. a:int B)$y)")] allE 1);
  10.198  by (asm_full_simp_tac (simpset() addsimps [ForallTL,ForallDropwhile])1);
  10.199  by (REPEAT (etac exE 1));
  10.200  by (REPEAT (etac conjE 1));
  10.201 @@ -311,7 +311,7 @@
  10.202  by (rotate_tac ~2 1); 
  10.203  by (Asm_full_simp_tac 1); 
  10.204  (* instantiate y1a and y2a *)
  10.205 -by (res_inst_tac [("x","Takewhile (%a. a:int B)`y @@ a>>y1")] exI 1);
  10.206 +by (res_inst_tac [("x","Takewhile (%a. a:int B)$y @@ a>>y1")] exI 1);
  10.207  by (res_inst_tac [("x","y2")] exI 1);
  10.208  (* elminate all obligations up to two depending on Conc_assoc *)
  10.209  by (asm_full_simp_tac (simpset() addsimps [ForallPTakewhileQ, intA_is_not_actB,
  10.210 @@ -328,11 +328,11 @@
  10.211  
  10.212  Goal " [| Finite as; is_asig(asig_of A); is_asig(asig_of B);compatible A B|] ==>  \
  10.213  \! x. Forall (%x. x:act A) x & Forall (%x. x:act A & x~:act B) as &\
  10.214 -\    Filter (%a. a:ext A)`x = Filter (%a. a:act A)`(as @@ z) \
  10.215 -\    --> (? x1 x2.  (mksch A B`(as @@ z)`x`y) = (x1 @@ (mksch A B`z`x2`y)) & \
  10.216 +\    Filter (%a. a:ext A)$x = Filter (%a. a:act A)$(as @@ z) \
  10.217 +\    --> (? x1 x2.  (mksch A B$(as @@ z)$x$y) = (x1 @@ (mksch A B$z$x2$y)) & \
  10.218  \                   Forall (%x. x:act A & x~:act B) x1 & \
  10.219  \                   Finite x1 & x = (x1 @@ x2) & \
  10.220 -\                   Filter (%a. a:ext A)`x1 = as)";
  10.221 +\                   Filter (%a. a:ext A)$x1 = as)";
  10.222  by (forw_inst_tac [("A1","A")] (compat_commute RS iffD1) 1);
  10.223  by (etac Seq_Finite_ind  1);
  10.224  by (REPEAT (rtac allI 1));
  10.225 @@ -351,12 +351,12 @@
  10.226  by (REPEAT (etac conjE 1));
  10.227  (* transform assumption f eA x = f A (s@z) *)
  10.228  by (dres_inst_tac [("x","x"),
  10.229 -                   ("g","Filter (%a. a:act A)`(s@@z)")] subst_lemma2 1);
  10.230 +                   ("g","Filter (%a. a:act A)$(s@@z)")] subst_lemma2 1);
  10.231  by (assume_tac 1);
  10.232  Addsimps [FilterConc]; 
  10.233  by (asm_full_simp_tac (simpset() addsimps [not_ext_is_int_or_not_act]) 1);
  10.234  (* apply IH *)
  10.235 -by (eres_inst_tac [("x","TL`(Dropwhile (%a. a:int A)`x)")] allE 1);
  10.236 +by (eres_inst_tac [("x","TL$(Dropwhile (%a. a:int A)$x)")] allE 1);
  10.237  by (asm_full_simp_tac (simpset() addsimps [ForallTL,ForallDropwhile])1);
  10.238  by (REPEAT (etac exE 1));
  10.239  by (REPEAT (etac conjE 1));
  10.240 @@ -365,7 +365,7 @@
  10.241  by (rotate_tac ~2 1); 
  10.242  by (Asm_full_simp_tac 1); 
  10.243  (* instantiate y1a and y2a *)
  10.244 -by (res_inst_tac [("x","Takewhile (%a. a:int A)`x @@ a>>x1")] exI 1);
  10.245 +by (res_inst_tac [("x","Takewhile (%a. a:int A)$x @@ a>>x1")] exI 1);
  10.246  by (res_inst_tac [("x","x2")] exI 1);
  10.247  (* elminate all obligations up to two depending on Conc_assoc *)
  10.248  by (asm_full_simp_tac (simpset() addsimps [ForallPTakewhileQ, intA_is_not_actB,
  10.249 @@ -380,7 +380,7 @@
  10.250  
  10.251  
  10.252  Goal "Finite y ==> ! z tr. Forall (%a.a:ext (A||B)) tr & \
  10.253 -\                             y = z @@ mksch A B`tr`a`b\
  10.254 +\                             y = z @@ mksch A B$tr$a$b\
  10.255  \                             --> Finite tr";
  10.256  by (etac Seq_Finite_ind  1);
  10.257  by Auto_tac;
  10.258 @@ -422,7 +422,7 @@
  10.259  by (rotate_tac ~2 2);
  10.260  by (rotate_tac ~2 3);
  10.261  by (asm_full_simp_tac (HOL_basic_ss addsimps [mksch_cons3]) 2);
  10.262 -by (eres_inst_tac [("x","sb@@Takewhile (%a. a: int A)`a @@ Takewhile (%a. a:int B)`b@@(aaa>>nil)")] allE 2);
  10.263 +by (eres_inst_tac [("x","sb@@Takewhile (%a. a: int A)$a @@ Takewhile (%a. a:int B)$b@@(aaa>>nil)")] allE 2);
  10.264  by (eres_inst_tac [("x","sa")] allE 2);
  10.265  by (asm_full_simp_tac (simpset() addsimps [Conc_assoc])2);
  10.266  
  10.267 @@ -455,7 +455,7 @@
  10.268  qed"FiniteConcUU";
  10.269  
  10.270  finiteR_mksch
  10.271 -  "Finite (mksch A B`tr`x`y) --> Finite tr"
  10.272 +  "Finite (mksch A B$tr$x$y) --> Finite tr"
  10.273  *)
  10.274  
  10.275  
  10.276 @@ -470,9 +470,9 @@
  10.277  \           is_asig(asig_of A); is_asig(asig_of B) |] ==> \
  10.278  \ ! schA schB. Forall (%x. x:act A) schA & Forall (%x. x:act B) schB & \
  10.279  \ Forall (%x. x:ext (A||B)) tr & \
  10.280 -\ Filter (%a. a:act A)`tr << Filter (%a. a:ext A)`schA &\
  10.281 -\ Filter (%a. a:act B)`tr << Filter (%a. a:ext B)`schB  \
  10.282 -\ --> Filter (%a. a:ext (A||B))`(mksch A B`tr`schA`schB) = tr";
  10.283 +\ Filter (%a. a:act A)$tr << Filter (%a. a:ext A)$schA &\
  10.284 +\ Filter (%a. a:act B)$tr << Filter (%a. a:ext B)$schB  \
  10.285 +\ --> Filter (%a. a:ext (A||B))$(mksch A B$tr$schA$schB) = tr";
  10.286  
  10.287  by (Seq_induct_tac "tr" [Forall_def,sforall_def,mksch_def] 1);
  10.288  
  10.289 @@ -546,10 +546,10 @@
  10.290  \ is_asig(asig_of A); is_asig(asig_of B) |] ==> \
  10.291  \ Forall (%x. x:ext (A||B)) tr & \
  10.292  \ Forall (%x. x:act A) schA & Forall (%x. x:act B) schB & \
  10.293 -\ Filter (%a. a:ext A)`schA = Filter (%a. a:act A)`tr &\
  10.294 -\ Filter (%a. a:ext B)`schB = Filter (%a. a:act B)`tr &\
  10.295 +\ Filter (%a. a:ext A)$schA = Filter (%a. a:act A)$tr &\
  10.296 +\ Filter (%a. a:ext B)$schB = Filter (%a. a:act B)$tr &\
  10.297  \ LastActExtsch A schA & LastActExtsch B schB  \
  10.298 -\ --> Filter (%a. a:act A)`(mksch A B`tr`schA`schB) = schA";
  10.299 +\ --> Filter (%a. a:act A)$(mksch A B$tr$schA$schB) = schA";
  10.300  
  10.301  by (res_inst_tac [("Q","%x. x:act B & x~:act A"),("x","tr")] take_lemma_less_induct 1);
  10.302  by (REPEAT (etac conjE 1));
  10.303 @@ -600,7 +600,7 @@
  10.304  
  10.305  (* eliminate the B-only prefix *)
  10.306  
  10.307 -by (subgoal_tac "(Filter (%a. a :act A)`y1) = nil" 1);
  10.308 +by (subgoal_tac "(Filter (%a. a :act A)$y1) = nil" 1);
  10.309  by (etac ForallQFilterPnil 2);
  10.310  by (assume_tac 2);
  10.311  by (Fast_tac 2);
  10.312 @@ -613,7 +613,7 @@
  10.313  by (rotate_tac ~2 1);
  10.314  by (Asm_full_simp_tac 1);
  10.315  
  10.316 -by (subgoal_tac "Filter (%a. a:act A & a:ext B)`y1=nil" 1);
  10.317 +by (subgoal_tac "Filter (%a. a:act A & a:ext B)$y1=nil" 1);
  10.318  by (rotate_tac ~1 1);
  10.319  by (Asm_full_simp_tac  1);
  10.320  (* eliminate introduced subgoal 2 *)
  10.321 @@ -651,7 +651,7 @@
  10.322  by (asm_full_simp_tac (simpset() addsimps [ext_and_act]) 1);
  10.323  (* assumption schA *)
  10.324  by (dres_inst_tac [("x","schA"),
  10.325 -                   ("g","Filter (%a. a:act A)`s2")] subst_lemma2 1);
  10.326 +                   ("g","Filter (%a. a:act A)$s2")] subst_lemma2 1);
  10.327  by (assume_tac 1);
  10.328  by (Asm_full_simp_tac 1);
  10.329  (* assumptions concerning LastActExtsch, cannot be rewritten, as LastActExtsmalli are looping  *)
  10.330 @@ -680,10 +680,10 @@
  10.331  \ is_asig(asig_of A); is_asig(asig_of B) |] ==> \
  10.332  \ Forall (%x. x:ext (A||B)) tr & \
  10.333  \ Forall (%x. x:act A) schA & Forall (%x. x:act B) schB & \
  10.334 -\ Filter (%a. a:ext A)`schA = Filter (%a. a:act A)`tr &\
  10.335 -\ Filter (%a. a:ext B)`schB = Filter (%a. a:act B)`tr &\
  10.336 +\ Filter (%a. a:ext A)$schA = Filter (%a. a:act A)$tr &\
  10.337 +\ Filter (%a. a:ext B)$schB = Filter (%a. a:act B)$tr &\
  10.338  \ LastActExtsch A schA & LastActExtsch B schB  \
  10.339 -\ --> Filter (%a. a:act A)`(mksch A B`tr`schA`schB) = schA";
  10.340 +\ --> Filter (%a. a:act A)$(mksch A B$tr$schA$schB) = schA";
  10.341  
  10.342  by (strip_tac 1);
  10.343  by (resolve_tac seq.take_lemmas 1);
  10.344 @@ -756,7 +756,7 @@
  10.345  
  10.346  (* eliminate the B-only prefix *)
  10.347  
  10.348 -by (subgoal_tac "(Filter (%a. a :act A)`y1) = nil" 1);
  10.349 +by (subgoal_tac "(Filter (%a. a :act A)$y1) = nil" 1);
  10.350  by (etac ForallQFilterPnil 2);
  10.351  by (assume_tac 2);
  10.352  by (Fast_tac 2);
  10.353 @@ -769,7 +769,7 @@
  10.354  by (rotate_tac ~2 1);
  10.355  by (Asm_full_simp_tac 1);
  10.356  
  10.357 -by (subgoal_tac "Filter (%a. a:act A & a:ext B)`y1=nil" 1);
  10.358 +by (subgoal_tac "Filter (%a. a:act A & a:ext B)$y1=nil" 1);
  10.359  by (rotate_tac ~1 1);
  10.360  by (Asm_full_simp_tac  1);
  10.361  (* eliminate introduced subgoal 2 *)
  10.362 @@ -808,7 +808,7 @@
  10.363  by (REPEAT (etac conjE 1));
  10.364  (* assumption schA *)
  10.365  by (dres_inst_tac [("x","schA"),
  10.366 -                   ("g","Filter (%a. a:act A)`rs")] subst_lemma2 1);
  10.367 +                   ("g","Filter (%a. a:act A)$rs")] subst_lemma2 1);
  10.368  by (assume_tac 1);
  10.369  by (asm_full_simp_tac (simpset() addsimps [int_is_not_ext]) 1);
  10.370  (* assumptions concerning LastActExtsch, cannot be rewritten, as LastActExtsmalli are looping  *)
  10.371 @@ -828,7 +828,7 @@
  10.372  by (rotate_tac ~2 1);
  10.373  by (Asm_full_simp_tac  1);
  10.374  
  10.375 -by (subgoal_tac "Filter (%a. a:act A & a:ext B)`y1=nil" 1);
  10.376 +by (subgoal_tac "Filter (%a. a:act A & a:ext B)$y1=nil" 1);
  10.377  by (rotate_tac ~1 1);
  10.378  by (Asm_full_simp_tac  1);
  10.379  (* eliminate introduced subgoal 2 *)
  10.380 @@ -860,7 +860,7 @@
  10.381  by (REPEAT (etac conjE 1));
  10.382  (* assumption schA *)
  10.383  by (dres_inst_tac [("x","schA"),
  10.384 -                   ("g","Filter (%a. a:act A)`rs")] subst_lemma2 1);
  10.385 +                   ("g","Filter (%a. a:act A)$rs")] subst_lemma2 1);
  10.386  by (assume_tac 1);
  10.387  by (asm_full_simp_tac (simpset() addsimps [int_is_not_ext]) 1);
  10.388  
  10.389 @@ -878,7 +878,7 @@
  10.390  
  10.391  (* assumption schB *)
  10.392  by (dres_inst_tac [("x","y2"),
  10.393 -                   ("g","Filter (%a. a:act B)`rs")] subst_lemma2 1);
  10.394 +                   ("g","Filter (%a. a:act B)$rs")] subst_lemma2 1);
  10.395  by (assume_tac 1);
  10.396  by (asm_full_simp_tac (simpset() addsimps [intA_is_not_actB,int_is_not_ext]) 1);
  10.397  
  10.398 @@ -920,10 +920,10 @@
  10.399  \ is_asig(asig_of A); is_asig(asig_of B) |] ==> \
  10.400  \ Forall (%x. x:ext (A||B)) tr & \
  10.401  \ Forall (%x. x:act A) schA & Forall (%x. x:act B) schB & \
  10.402 -\ Filter (%a. a:ext A)`schA = Filter (%a. a:act A)`tr &\
  10.403 -\ Filter (%a. a:ext B)`schB = Filter (%a. a:act B)`tr &\
  10.404 +\ Filter (%a. a:ext A)$schA = Filter (%a. a:act A)$tr &\
  10.405 +\ Filter (%a. a:ext B)$schB = Filter (%a. a:act B)$tr &\
  10.406  \ LastActExtsch A schA & LastActExtsch B schB  \
  10.407 -\ --> Filter (%a. a:act B)`(mksch A B`tr`schA`schB) = schB";
  10.408 +\ --> Filter (%a. a:act B)$(mksch A B$tr$schA$schB) = schB";
  10.409  
  10.410  by (strip_tac 1);
  10.411  by (resolve_tac seq.take_lemmas 1);
  10.412 @@ -998,7 +998,7 @@
  10.413  
  10.414  (* eliminate the A-only prefix *)
  10.415  
  10.416 -by (subgoal_tac "(Filter (%a. a :act B)`x1) = nil" 1);
  10.417 +by (subgoal_tac "(Filter (%a. a :act B)$x1) = nil" 1);
  10.418  by (etac ForallQFilterPnil 2);
  10.419  by (assume_tac 2);
  10.420  by (Fast_tac 2);
  10.421 @@ -1011,7 +1011,7 @@
  10.422  by (rotate_tac ~2 1);
  10.423  by (Asm_full_simp_tac 1);
  10.424  
  10.425 -by (subgoal_tac "Filter (%a. a:act B & a:ext A)`x1=nil" 1);
  10.426 +by (subgoal_tac "Filter (%a. a:act B & a:ext A)$x1=nil" 1);
  10.427  by (rotate_tac ~1 1);
  10.428  by (Asm_full_simp_tac  1);
  10.429  (* eliminate introduced subgoal 2 *)
  10.430 @@ -1050,7 +1050,7 @@
  10.431  by (REPEAT (etac conjE 1));
  10.432  (* assumption schB *)
  10.433  by (dres_inst_tac [("x","schB"),
  10.434 -                   ("g","Filter (%a. a:act B)`rs")] subst_lemma2 1);
  10.435 +                   ("g","Filter (%a. a:act B)$rs")] subst_lemma2 1);
  10.436  by (assume_tac 1);
  10.437  by (asm_full_simp_tac (simpset() addsimps [int_is_not_ext]) 1);
  10.438  (* assumptions concerning LastActExtsch, cannot be rewritten, as LastActExtsmalli are looping  *)
  10.439 @@ -1070,7 +1070,7 @@
  10.440  by (rotate_tac ~2 1);
  10.441  by (Asm_full_simp_tac  1);
  10.442  
  10.443 -by (subgoal_tac "Filter (%a. a:act B & a:ext A)`x1=nil" 1);
  10.444 +by (subgoal_tac "Filter (%a. a:act B & a:ext A)$x1=nil" 1);
  10.445  by (rotate_tac ~1 1);
  10.446  by (Asm_full_simp_tac  1);
  10.447  (* eliminate introduced subgoal 2 *)
  10.448 @@ -1102,7 +1102,7 @@
  10.449  by (REPEAT (etac conjE 1));
  10.450  (* assumption schA *)
  10.451  by (dres_inst_tac [("x","schB"),
  10.452 -                   ("g","Filter (%a. a:act B)`rs")] subst_lemma2 1);
  10.453 +                   ("g","Filter (%a. a:act B)$rs")] subst_lemma2 1);
  10.454  by (assume_tac 1);
  10.455  by (asm_full_simp_tac (simpset() addsimps [int_is_not_ext]) 1);
  10.456  
  10.457 @@ -1120,7 +1120,7 @@
  10.458  
  10.459  (* assumption schA *)
  10.460  by (dres_inst_tac [("x","x2"),
  10.461 -                   ("g","Filter (%a. a:act A)`rs")] subst_lemma2 1);
  10.462 +                   ("g","Filter (%a. a:act A)$rs")] subst_lemma2 1);
  10.463  by (assume_tac 1);
  10.464  by (asm_full_simp_tac (simpset() addsimps [intA_is_not_actB,int_is_not_ext]) 1);
  10.465  
  10.466 @@ -1158,8 +1158,8 @@
  10.467  "!! A B. [| is_trans_of A; is_trans_of B; compatible A B; compatible B A; \
  10.468  \           is_asig(asig_of A); is_asig(asig_of B)|] \
  10.469  \       ==>  tr: traces(A||B) = \
  10.470 -\            (Filter (%a. a:act A)`tr : traces A &\
  10.471 -\             Filter (%a. a:act B)`tr : traces B &\
  10.472 +\            (Filter (%a. a:act A)$tr : traces A &\
  10.473 +\             Filter (%a. a:act B)$tr : traces B &\
  10.474  \             Forall (%x. x:ext(A||B)) tr)";
  10.475  
  10.476  by (simp_tac (simpset() addsimps [traces_def,has_trace_def]) 1);
  10.477 @@ -1167,12 +1167,12 @@
  10.478   
  10.479  (* ==> *) 
  10.480  (* There is a schedule of A *)
  10.481 -by (res_inst_tac [("x","Filter (%a. a:act A)`sch")] bexI 1);
  10.482 +by (res_inst_tac [("x","Filter (%a. a:act A)$sch")] bexI 1);
  10.483  by (asm_full_simp_tac (simpset() addsimps [compositionality_sch]) 2);
  10.484  by (asm_full_simp_tac (simpset() addsimps [compatibility_consequence1,
  10.485                    externals_of_par,ext1_ext2_is_not_act1]) 1);
  10.486  (* There is a schedule of B *)
  10.487 -by (res_inst_tac [("x","Filter (%a. a:act B)`sch")] bexI 1);
  10.488 +by (res_inst_tac [("x","Filter (%a. a:act B)$sch")] bexI 1);
  10.489  by (asm_full_simp_tac (simpset() addsimps [compositionality_sch]) 2);
  10.490  by (asm_full_simp_tac (simpset() addsimps [compatibility_consequence2,
  10.491                    externals_of_par,ext1_ext2_is_not_act2]) 1);
  10.492 @@ -1197,7 +1197,7 @@
  10.493  ren "h1 h2 schA schB" 1;
  10.494  (* mksch is exactly the construction of trA||B out of schA, schB, and the oracle tr,
  10.495     we need here *)
  10.496 -by (res_inst_tac [("x","mksch A B`tr`schA`schB")] bexI 1);
  10.497 +by (res_inst_tac [("x","mksch A B$tr$schA$schB")] bexI 1);
  10.498  
  10.499  (* External actions of mksch are just the oracle *)
  10.500  by (asm_full_simp_tac (simpset() addsimps [FilterA_mksch_is_tr RS spec RS spec RS mp]) 1);
    11.1 --- a/src/HOLCF/IOA/meta_theory/CompoTraces.thy	Tue Jan 09 15:32:27 2001 +0100
    11.2 +++ b/src/HOLCF/IOA/meta_theory/CompoTraces.thy	Tue Jan 09 15:36:30 2001 +0100
    11.3 @@ -17,7 +17,7 @@
    11.4  defs
    11.5  
    11.6  mksch_def
    11.7 -  "mksch A B == (fix`(LAM h tr schA schB. case tr of 
    11.8 +  "mksch A B == (fix$(LAM h tr schA schB. case tr of 
    11.9         nil => nil
   11.10      | x##xs => 
   11.11        (case x of 
   11.12 @@ -25,24 +25,24 @@
   11.13        | Def y => 
   11.14           (if y:act A then 
   11.15               (if y:act B then 
   11.16 -                   ((Takewhile (%a. a:int A)`schA)
   11.17 -                      @@ (Takewhile (%a. a:int B)`schB)
   11.18 -                           @@ (y>>(h`xs
   11.19 -                                    `(TL`(Dropwhile (%a. a:int A)`schA))
   11.20 -                                    `(TL`(Dropwhile (%a. a:int B)`schB))
   11.21 +                   ((Takewhile (%a. a:int A)$schA)
   11.22 +                      @@ (Takewhile (%a. a:int B)$schB)
   11.23 +                           @@ (y>>(h$xs
   11.24 +                                    $(TL$(Dropwhile (%a. a:int A)$schA))
   11.25 +                                    $(TL$(Dropwhile (%a. a:int B)$schB))
   11.26                      )))
   11.27                else
   11.28 -                 ((Takewhile (%a. a:int A)`schA)
   11.29 -                  @@ (y>>(h`xs
   11.30 -                           `(TL`(Dropwhile (%a. a:int A)`schA))
   11.31 -                           `schB)))
   11.32 +                 ((Takewhile (%a. a:int A)$schA)
   11.33 +                  @@ (y>>(h$xs
   11.34 +                           $(TL$(Dropwhile (%a. a:int A)$schA))
   11.35 +                           $schB)))
   11.36                )
   11.37            else 
   11.38               (if y:act B then 
   11.39 -                 ((Takewhile (%a. a:int B)`schB)
   11.40 -                     @@ (y>>(h`xs
   11.41 -                              `schA
   11.42 -                              `(TL`(Dropwhile (%a. a:int B)`schB))
   11.43 +                 ((Takewhile (%a. a:int B)$schB)
   11.44 +                     @@ (y>>(h$xs
   11.45 +                              $schA
   11.46 +                              $(TL$(Dropwhile (%a. a:int B)$schB))
   11.47                                )))
   11.48               else
   11.49                 UU
   11.50 @@ -56,8 +56,8 @@
   11.51         let trA = fst TracesA; sigA = snd TracesA; 
   11.52             trB = fst TracesB; sigB = snd TracesB       
   11.53         in
   11.54 -       (    {tr. Filter (%a. a:actions sigA)`tr : trA}
   11.55 -        Int {tr. Filter (%a. a:actions sigB)`tr : trB}
   11.56 +       (    {tr. Filter (%a. a:actions sigA)$tr : trA}
   11.57 +        Int {tr. Filter (%a. a:actions sigB)$tr : trB}
   11.58          Int {tr. Forall (%x. x:(externals sigA Un externals sigB)) tr},
   11.59          asig_comp sigA sigB)"
   11.60  
   11.61 @@ -65,7 +65,7 @@
   11.62  
   11.63  
   11.64  finiteR_mksch
   11.65 -  "Finite (mksch A B`tr`x`y) --> Finite tr"
   11.66 +  "Finite (mksch A B$tr$x$y) --> Finite tr"
   11.67  
   11.68  
   11.69  
    12.1 --- a/src/HOLCF/IOA/meta_theory/Compositionality.ML	Tue Jan 09 15:32:27 2001 +0100
    12.2 +++ b/src/HOLCF/IOA/meta_theory/Compositionality.ML	Tue Jan 09 15:36:30 2001 +0100
    12.3 @@ -15,9 +15,9 @@
    12.4  
    12.5  Goal 
    12.6  "!! A B. [| compatible A B; Forall (%a. a: ext A | a: ext B) tr |] ==> \
    12.7 -\           Filter (%a. a: act A)`tr= Filter (%a. a: ext A)`tr";
    12.8 +\           Filter (%a. a: act A)$tr= Filter (%a. a: ext A)$tr";
    12.9  by (rtac ForallPFilterQR 1);
   12.10 -(* i.e.: [| (! x. P x --> (Q x = R x)) ; Forall P tr |] ==> Filter Q`tr = Filter R`tr *)
   12.11 +(* i.e.: [| (! x. P x --> (Q x = R x)) ; Forall P tr |] ==> Filter Q$tr = Filter R$tr *)
   12.12  by (assume_tac 2);
   12.13  by (rtac compatibility_consequence3 1);
   12.14  by (REPEAT (asm_full_simp_tac (simpset() 
   12.15 @@ -32,7 +32,7 @@
   12.16  qed"compatibility_consequence4";
   12.17  
   12.18  Goal "[| compatible A B; Forall (%a. a: ext B | a: ext A) tr |] ==> \
   12.19 -\           Filter (%a. a: act A)`tr= Filter (%a. a: ext A)`tr";
   12.20 +\           Filter (%a. a: act A)$tr= Filter (%a. a: ext A)$tr";
   12.21  by (rtac ForallPFilterQR 1);
   12.22  by (assume_tac 2);
   12.23  by (rtac compatibility_consequence4 1);
    13.1 --- a/src/HOLCF/IOA/meta_theory/Deadlock.ML	Tue Jan 09 15:32:27 2001 +0100
    13.2 +++ b/src/HOLCF/IOA/meta_theory/Deadlock.ML	Tue Jan 09 15:36:30 2001 +0100
    13.3 @@ -10,8 +10,8 @@
    13.4                 input actions may always be added to a schedule
    13.5  **********************************************************************************)
    13.6  
    13.7 -Goal "[| Filter (%x. x:act A)`sch : schedules A; a:inp A; input_enabled A; Finite sch|] \
    13.8 -\         ==> Filter (%x. x:act A)`sch @@ a>>nil : schedules A";
    13.9 +Goal "[| Filter (%x. x:act A)$sch : schedules A; a:inp A; input_enabled A; Finite sch|] \
   13.10 +\         ==> Filter (%x. x:act A)$sch @@ a>>nil : schedules A";
   13.11  by (asm_full_simp_tac (simpset() addsimps [schedules_def,has_schedule_def]) 1);
   13.12  by (safe_tac set_cs);
   13.13  by (ftac inp_is_act 1);
   13.14 @@ -21,7 +21,7 @@
   13.15  by (subgoal_tac "Finite ex" 1);
   13.16  by (asm_full_simp_tac (simpset() addsimps [filter_act_def]) 2);
   13.17  by (rtac (Map2Finite RS iffD1) 2);
   13.18 -by (res_inst_tac [("t","Map fst`ex")] subst 2);
   13.19 +by (res_inst_tac [("t","Map fst$ex")] subst 2);
   13.20  by (assume_tac 2);
   13.21  by (etac FiniteFilter 2);
   13.22  (* subgoal 1 *)
   13.23 @@ -52,7 +52,7 @@
   13.24  **********************************************************************************)
   13.25  Delsplits [split_if];
   13.26  Goal "[| a : local A; Finite sch; sch : schedules (A||B); \
   13.27 -\            Filter (%x. x:act A)`(sch @@ a>>nil) : schedules A; compatible A B; input_enabled B |] \
   13.28 +\            Filter (%x. x:act A)$(sch @@ a>>nil) : schedules A; compatible A B; input_enabled B |] \
   13.29  \          ==> (sch @@ a>>nil) : schedules (A||B)";
   13.30  
   13.31  by (asm_full_simp_tac (simpset() addsimps [compositionality_sch,locals_def]) 1);
    14.1 --- a/src/HOLCF/IOA/meta_theory/LiveIOA.thy	Tue Jan 09 15:32:27 2001 +0100
    14.2 +++ b/src/HOLCF/IOA/meta_theory/LiveIOA.thy	Tue Jan 09 15:36:30 2001 +0100
    14.3 @@ -45,7 +45,7 @@
    14.4     "liveexecutions AP == {exec. exec : executions (fst AP) & (exec |== (snd AP))}"
    14.5  
    14.6  livetraces_def
    14.7 -  "livetraces AP == {mk_trace (fst AP)`(snd ex) | ex. ex:liveexecutions AP}"
    14.8 +  "livetraces AP == {mk_trace (fst AP)$(snd ex) | ex. ex:liveexecutions AP}"
    14.9  
   14.10  live_implements_def
   14.11    "live_implements CL AM == (inp (fst CL) = inp (fst AM)) & 
    15.1 --- a/src/HOLCF/IOA/meta_theory/RefCorrectness.ML	Tue Jan 09 15:32:27 2001 +0100
    15.2 +++ b/src/HOLCF/IOA/meta_theory/RefCorrectness.ML	Tue Jan 09 15:36:30 2001 +0100
    15.3 @@ -21,8 +21,8 @@
    15.4  Goal "corresp_exC A f  = (LAM ex. (%s. case ex of \
    15.5  \      nil =>  nil   \
    15.6  \    | x##xs => (flift1 (%pr. (@cex. move A cex (f s) (fst pr) (f (snd pr)))   \
    15.7 -\                              @@ ((corresp_exC A f `xs) (snd pr)))   \
    15.8 -\                        `x) ))";
    15.9 +\                              @@ ((corresp_exC A f $xs) (snd pr)))   \
   15.10 +\                        $x) ))";
   15.11  by (rtac trans 1);
   15.12  by (rtac fix_eq2 1);
   15.13  by (rtac corresp_exC_def 1);
   15.14 @@ -30,19 +30,19 @@
   15.15  by (simp_tac (simpset() addsimps [flift1_def]) 1);
   15.16  qed"corresp_exC_unfold";
   15.17  
   15.18 -Goal "(corresp_exC A f`UU) s=UU";
   15.19 +Goal "(corresp_exC A f$UU) s=UU";
   15.20  by (stac corresp_exC_unfold 1);
   15.21  by (Simp_tac 1);
   15.22  qed"corresp_exC_UU";
   15.23  
   15.24 -Goal "(corresp_exC A f`nil) s = nil";
   15.25 +Goal "(corresp_exC A f$nil) s = nil";
   15.26  by (stac corresp_exC_unfold 1);
   15.27  by (Simp_tac 1);
   15.28  qed"corresp_exC_nil";
   15.29  
   15.30 -Goal "(corresp_exC A f`(at>>xs)) s = \
   15.31 +Goal "(corresp_exC A f$(at>>xs)) s = \
   15.32  \          (@cex. move A cex (f s) (fst at) (f (snd at)))  \
   15.33 -\          @@ ((corresp_exC A f`xs) (snd at))";
   15.34 +\          @@ ((corresp_exC A f$xs) (snd at))";
   15.35  by (rtac trans 1);
   15.36  by (stac corresp_exC_unfold 1);
   15.37  by (asm_full_simp_tac (simpset() addsimps [Consq_def,flift1_def]) 1);
   15.38 @@ -98,7 +98,7 @@
   15.39  
   15.40  Goal
   15.41     "[|is_ref_map f C A; reachable C s; (s,a,t):trans_of C|] ==>\
   15.42 -\     mk_trace A`((@x. move A x (f s) a (f t))) = \
   15.43 +\     mk_trace A$((@x. move A x (f s) a (f t))) = \
   15.44  \       (if a:ext A then a>>nil else nil)";
   15.45  
   15.46  by (cut_inst_tac [] move_is_move 1);
   15.47 @@ -119,7 +119,7 @@
   15.48  (* --------------------------------------------------- *)
   15.49  
   15.50  
   15.51 -Goal "mk_trace C`(ex1 @@ ex2)= (mk_trace C`ex1) @@ (mk_trace C`ex2)";
   15.52 +Goal "mk_trace C$(ex1 @@ ex2)= (mk_trace C$ex1) @@ (mk_trace C$ex2)";
   15.53  by (simp_tac (simpset() addsimps [mk_trace_def,filter_act_def,
   15.54                                   FilterConc,MapConc]) 1);
   15.55  qed"mk_traceConc";
   15.56 @@ -133,7 +133,7 @@
   15.57  Goalw [corresp_ex_def]
   15.58    "[|is_ref_map f C A; ext C = ext A|] ==>  \     
   15.59  \        !s. reachable C s & is_exec_frag C (s,xs) --> \
   15.60 -\            mk_trace C`xs = mk_trace A`(snd (corresp_ex A f (s,xs)))";
   15.61 +\            mk_trace C$xs = mk_trace A$(snd (corresp_ex A f (s,xs)))";
   15.62  
   15.63  by (pair_induct_tac "xs" [is_exec_frag_def] 1);
   15.64  (* cons case *) 
    16.1 --- a/src/HOLCF/IOA/meta_theory/RefCorrectness.thy	Tue Jan 09 15:32:27 2001 +0100
    16.2 +++ b/src/HOLCF/IOA/meta_theory/RefCorrectness.thy	Tue Jan 09 15:36:30 2001 +0100
    16.3 @@ -20,15 +20,15 @@
    16.4  defs
    16.5  
    16.6  corresp_ex_def
    16.7 -  "corresp_ex A f ex == (f (fst ex),(corresp_exC A f`(snd ex)) (fst ex))"
    16.8 +  "corresp_ex A f ex == (f (fst ex),(corresp_exC A f$(snd ex)) (fst ex))"
    16.9  
   16.10  
   16.11  corresp_exC_def
   16.12 -  "corresp_exC A f  == (fix`(LAM h ex. (%s. case ex of 
   16.13 +  "corresp_exC A f  == (fix$(LAM h ex. (%s. case ex of 
   16.14        nil =>  nil
   16.15      | x##xs => (flift1 (%pr. (@cex. move A cex (f s) (fst pr) (f (snd pr)))
   16.16 -                              @@ ((h`xs) (snd pr)))
   16.17 -                        `x) )))"
   16.18 +                              @@ ((h$xs) (snd pr)))
   16.19 +                        $x) )))"
   16.20   
   16.21  is_fair_ref_map_def
   16.22    "is_fair_ref_map f C A == 
    17.1 --- a/src/HOLCF/IOA/meta_theory/RefMappings.thy	Tue Jan 09 15:32:27 2001 +0100
    17.2 +++ b/src/HOLCF/IOA/meta_theory/RefMappings.thy	Tue Jan 09 15:36:30 2001 +0100
    17.3 @@ -24,7 +24,7 @@
    17.4    "move ioa ex s a t ==    
    17.5      (is_exec_frag ioa (s,ex) &  Finite ex & 
    17.6       laststate (s,ex)=t  &     
    17.7 -     mk_trace ioa`ex = (if a:ext(ioa) then a>>nil else nil))"
    17.8 +     mk_trace ioa$ex = (if a:ext(ioa) then a>>nil else nil))"
    17.9  
   17.10  is_ref_map_def
   17.11    "is_ref_map f C A ==                          
    18.1 --- a/src/HOLCF/IOA/meta_theory/Seq.ML	Tue Jan 09 15:32:27 2001 +0100
    18.2 +++ b/src/HOLCF/IOA/meta_theory/Seq.ML	Tue Jan 09 15:36:30 2001 +0100
    18.3 @@ -34,20 +34,20 @@
    18.4  bind_thm ("smap_unfold", fix_prover2 thy smap_def 
    18.5     "smap = (LAM f tr. case tr of  \
    18.6   \                         nil  => nil \
    18.7 - \                       | x##xs => f`x ## smap`f`xs)");
    18.8 + \                       | x##xs => f$x ## smap$f$xs)");
    18.9  
   18.10 -Goal "smap`f`nil=nil"; 
   18.11 +Goal "smap$f$nil=nil"; 
   18.12  by (stac smap_unfold 1);
   18.13  by (Simp_tac 1);
   18.14  qed"smap_nil";
   18.15  
   18.16 -Goal "smap`f`UU=UU"; 
   18.17 +Goal "smap$f$UU=UU"; 
   18.18  by (stac smap_unfold 1);
   18.19  by (Simp_tac 1);
   18.20  qed"smap_UU";
   18.21  
   18.22  Goal 
   18.23 -"[|x~=UU|] ==> smap`f`(x##xs)= (f`x)##smap`f`xs"; 
   18.24 +"[|x~=UU|] ==> smap$f$(x##xs)= (f$x)##smap$f$xs"; 
   18.25  by (rtac trans 1);
   18.26  by (stac smap_unfold 1);
   18.27  by (Asm_full_simp_tac 1);
   18.28 @@ -61,21 +61,21 @@
   18.29  bind_thm ("sfilter_unfold", fix_prover2 thy sfilter_def 
   18.30    "sfilter = (LAM P tr. case tr of  \
   18.31   \         nil   => nil \
   18.32 - \       | x##xs => If P`x then x##(sfilter`P`xs) else sfilter`P`xs fi)");
   18.33 + \       | x##xs => If P$x then x##(sfilter$P$xs) else sfilter$P$xs fi)");
   18.34  
   18.35 -Goal "sfilter`P`nil=nil";
   18.36 +Goal "sfilter$P$nil=nil";
   18.37  by (stac sfilter_unfold 1);
   18.38  by (Simp_tac 1);
   18.39  qed"sfilter_nil";
   18.40  
   18.41 -Goal "sfilter`P`UU=UU";
   18.42 +Goal "sfilter$P$UU=UU";
   18.43  by (stac sfilter_unfold 1);
   18.44  by (Simp_tac 1);
   18.45  qed"sfilter_UU";
   18.46  
   18.47  Goal 
   18.48 -"x~=UU ==> sfilter`P`(x##xs)=   \
   18.49 -\             (If P`x then x##(sfilter`P`xs) else sfilter`P`xs fi)";
   18.50 +"x~=UU ==> sfilter$P$(x##xs)=   \
   18.51 +\             (If P$x then x##(sfilter$P$xs) else sfilter$P$xs fi)";
   18.52  by (rtac trans 1);
   18.53  by (stac sfilter_unfold 1);
   18.54  by (Asm_full_simp_tac 1);
   18.55 @@ -89,20 +89,20 @@
   18.56  bind_thm ("sforall2_unfold", fix_prover2 thy sforall2_def 
   18.57     "sforall2 = (LAM P tr. case tr of  \
   18.58   \                         nil   => TT \
   18.59 - \                       | x##xs => (P`x andalso sforall2`P`xs))");
   18.60 + \                       | x##xs => (P$x andalso sforall2$P$xs))");
   18.61  
   18.62 -Goal "sforall2`P`nil=TT"; 
   18.63 +Goal "sforall2$P$nil=TT"; 
   18.64  by (stac sforall2_unfold 1);
   18.65  by (Simp_tac 1);
   18.66  qed"sforall2_nil";
   18.67  
   18.68 -Goal "sforall2`P`UU=UU"; 
   18.69 +Goal "sforall2$P$UU=UU"; 
   18.70  by (stac sforall2_unfold 1);
   18.71  by (Simp_tac 1);
   18.72  qed"sforall2_UU";
   18.73  
   18.74  Goal 
   18.75 -"x~=UU ==> sforall2`P`(x##xs)= ((P`x) andalso sforall2`P`xs)";
   18.76 +"x~=UU ==> sforall2$P$(x##xs)= ((P$x) andalso sforall2$P$xs)";
   18.77  by (rtac trans 1);
   18.78  by (stac sforall2_unfold 1);
   18.79  by (Asm_full_simp_tac 1);
   18.80 @@ -118,21 +118,21 @@
   18.81  bind_thm ("stakewhile_unfold", fix_prover2 thy stakewhile_def 
   18.82     "stakewhile = (LAM P tr. case tr of  \
   18.83   \                         nil   => nil \
   18.84 - \                       | x##xs => (If P`x then x##(stakewhile`P`xs) else nil fi))");
   18.85 + \                       | x##xs => (If P$x then x##(stakewhile$P$xs) else nil fi))");
   18.86  
   18.87 -Goal "stakewhile`P`nil=nil"; 
   18.88 +Goal "stakewhile$P$nil=nil"; 
   18.89  by (stac stakewhile_unfold 1);
   18.90  by (Simp_tac 1);
   18.91  qed"stakewhile_nil";
   18.92  
   18.93 -Goal "stakewhile`P`UU=UU"; 
   18.94 +Goal "stakewhile$P$UU=UU"; 
   18.95  by (stac stakewhile_unfold 1);
   18.96  by (Simp_tac 1);
   18.97  qed"stakewhile_UU";
   18.98  
   18.99  Goal 
  18.100 -"x~=UU ==> stakewhile`P`(x##xs) =   \
  18.101 -\             (If P`x then x##(stakewhile`P`xs) else nil fi)";
  18.102 +"x~=UU ==> stakewhile$P$(x##xs) =   \
  18.103 +\             (If P$x then x##(stakewhile$P$xs) else nil fi)";
  18.104  by (rtac trans 1);
  18.105  by (stac stakewhile_unfold 1);
  18.106  by (Asm_full_simp_tac 1);
  18.107 @@ -147,21 +147,21 @@
  18.108  bind_thm ("sdropwhile_unfold", fix_prover2 thy sdropwhile_def 
  18.109     "sdropwhile = (LAM P tr. case tr of  \
  18.110   \                         nil   => nil \
  18.111 - \                       | x##xs => (If P`x then sdropwhile`P`xs else tr fi))");
  18.112 + \                       | x##xs => (If P$x then sdropwhile$P$xs else tr fi))");
  18.113  
  18.114 -Goal "sdropwhile`P`nil=nil"; 
  18.115 +Goal "sdropwhile$P$nil=nil"; 
  18.116  by (stac sdropwhile_unfold 1);
  18.117  by (Simp_tac 1);
  18.118  qed"sdropwhile_nil";
  18.119  
  18.120 -Goal "sdropwhile`P`UU=UU"; 
  18.121 +Goal "sdropwhile$P$UU=UU"; 
  18.122  by (stac sdropwhile_unfold 1);
  18.123  by (Simp_tac 1);
  18.124  qed"sdropwhile_UU";
  18.125  
  18.126  Goal 
  18.127 -"x~=UU ==> sdropwhile`P`(x##xs) =   \
  18.128 -\             (If P`x then sdropwhile`P`xs else x##xs fi)";
  18.129 +"x~=UU ==> sdropwhile$P$(x##xs) =   \
  18.130 +\             (If P$x then sdropwhile$P$xs else x##xs fi)";
  18.131  by (rtac trans 1);
  18.132  by (stac sdropwhile_unfold 1);
  18.133  by (Asm_full_simp_tac 1);
  18.134 @@ -177,21 +177,21 @@
  18.135  bind_thm ("slast_unfold", fix_prover2 thy slast_def 
  18.136     "slast = (LAM tr. case tr of  \
  18.137   \                         nil   => UU \
  18.138 - \                       | x##xs => (If is_nil`xs then x else slast`xs fi))");
  18.139 + \                       | x##xs => (If is_nil$xs then x else slast$xs fi))");
  18.140  
  18.141  
  18.142 -Goal "slast`nil=UU"; 
  18.143 +Goal "slast$nil=UU"; 
  18.144  by (stac slast_unfold 1);
  18.145  by (Simp_tac 1);
  18.146  qed"slast_nil";
  18.147  
  18.148 -Goal "slast`UU=UU"; 
  18.149 +Goal "slast$UU=UU"; 
  18.150  by (stac slast_unfold 1);
  18.151  by (Simp_tac 1);
  18.152  qed"slast_UU";
  18.153  
  18.154  Goal 
  18.155 -"x~=UU ==> slast`(x##xs)= (If is_nil`xs then x else slast`xs fi)";
  18.156 +"x~=UU ==> slast$(x##xs)= (If is_nil$xs then x else slast$xs fi)";
  18.157  by (rtac trans 1);
  18.158  by (stac slast_unfold 1);
  18.159  by (Asm_full_simp_tac 1);
  18.160 @@ -237,19 +237,19 @@
  18.161  bind_thm ("sflat_unfold", fix_prover2 thy sflat_def 
  18.162     "sflat = (LAM tr. case tr of  \
  18.163   \                         nil   => nil \
  18.164 - \                       | x##xs => x @@ sflat`xs)");
  18.165 + \                       | x##xs => x @@ sflat$xs)");
  18.166  
  18.167 -Goal "sflat`nil=nil"; 
  18.168 +Goal "sflat$nil=nil"; 
  18.169  by (stac sflat_unfold 1);
  18.170  by (Simp_tac 1);
  18.171  qed"sflat_nil";
  18.172  
  18.173 -Goal "sflat`UU=UU"; 
  18.174 +Goal "sflat$UU=UU"; 
  18.175  by (stac sflat_unfold 1);
  18.176  by (Simp_tac 1);
  18.177  qed"sflat_UU";
  18.178  
  18.179 -Goal "sflat`(x##xs)= x@@(sflat`xs)"; 
  18.180 +Goal "sflat$(x##xs)= x@@(sflat$xs)"; 
  18.181  by (rtac trans 1);
  18.182  by (stac sflat_unfold 1);
  18.183  by (Asm_full_simp_tac 1);
  18.184 @@ -269,32 +269,32 @@
  18.185  \               nil   => nil    \
  18.186  \             | x##xs => (case t2 of     \
  18.187  \                          nil => UU    \
  18.188 -\                        | y##ys => <x,y>##(szip`xs`ys)))");
  18.189 +\                        | y##ys => <x,y>##(szip$xs$ys)))");
  18.190  
  18.191 -Goal "szip`nil`y=nil"; 
  18.192 +Goal "szip$nil$y=nil"; 
  18.193  by (stac szip_unfold 1);
  18.194  by (Simp_tac 1);
  18.195  qed"szip_nil";
  18.196  
  18.197 -Goal "szip`UU`y=UU"; 
  18.198 +Goal "szip$UU$y=UU"; 
  18.199  by (stac szip_unfold 1);
  18.200  by (Simp_tac 1);
  18.201  qed"szip_UU1";
  18.202  
  18.203 -Goal "x~=nil ==> szip`x`UU=UU"; 
  18.204 +Goal "x~=nil ==> szip$x$UU=UU"; 
  18.205  by (stac szip_unfold 1);
  18.206  by (Asm_full_simp_tac 1);
  18.207  by (res_inst_tac [("x","x")] seq.casedist 1);
  18.208  by (REPEAT (Asm_full_simp_tac 1));
  18.209  qed"szip_UU2";
  18.210  
  18.211 -Goal "x~=UU ==> szip`(x##xs)`nil=UU";
  18.212 +Goal "x~=UU ==> szip$(x##xs)$nil=UU";
  18.213  by (rtac trans 1);
  18.214  by (stac szip_unfold 1);
  18.215  by (REPEAT (Asm_full_simp_tac 1));
  18.216  qed"szip_cons_nil";
  18.217  
  18.218 -Goal "[| x~=UU; y~=UU|] ==> szip`(x##xs)`(y##ys) = <x,y>##szip`xs`ys";
  18.219 +Goal "[| x~=UU; y~=UU|] ==> szip$(x##xs)$(y##ys) = <x,y>##szip$xs$ys";
  18.220  by (rtac trans 1);
  18.221  by (stac szip_unfold 1);
  18.222  by (REPEAT (Asm_full_simp_tac 1));
  18.223 @@ -348,7 +348,7 @@
  18.224  Addsimps [if_and_sconc];
  18.225  
  18.226  
  18.227 -Goal "sfilter`P`(x @@ y) = (sfilter`P`x @@ sfilter`P`y)";
  18.228 +Goal "sfilter$P$(x @@ y) = (sfilter$P$x @@ sfilter$P$y)";
  18.229  
  18.230  by (res_inst_tac[("x","x")] seq.ind 1);
  18.231  (* adm *)
  18.232 @@ -360,7 +360,7 @@
  18.233  by (asm_full_simp_tac (simpset() setloop split_If_tac) 1);
  18.234  qed"sfiltersconc";
  18.235  
  18.236 -Goal "sforall P (stakewhile`P`x)";
  18.237 +Goal "sforall P (stakewhile$P$x)";
  18.238  by (simp_tac (simpset() addsimps [sforall_def]) 1);
  18.239  by (res_inst_tac[("x","x")] seq.ind 1);
  18.240  (* adm *)
  18.241 @@ -372,7 +372,7 @@
  18.242  by (asm_full_simp_tac (simpset() setloop split_If_tac) 1);
  18.243  qed"sforallPstakewhileP";
  18.244  
  18.245 -Goal "sforall P (sfilter`P`x)";
  18.246 +Goal "sforall P (sfilter$P$x)";
  18.247  by (simp_tac (simpset() addsimps [sforall_def]) 1);
  18.248  by (res_inst_tac[("x","x")] seq.ind 1);
  18.249  (* adm *)
  18.250 @@ -438,7 +438,7 @@
  18.251  
  18.252  
  18.253  qed_goalw "seq_finite_ind_lemma" thy  [seq.finite_def]
  18.254 -"(!!n. P(seq_take n`s)) ==>  seq_finite(s) -->P(s)"
  18.255 +"(!!n. P(seq_take n$s)) ==>  seq_finite(s) -->P(s)"
  18.256   (fn prems =>
  18.257          [
  18.258          (strip_tac 1),
    19.1 --- a/src/HOLCF/IOA/meta_theory/Seq.thy	Tue Jan 09 15:32:27 2001 +0100
    19.2 +++ b/src/HOLCF/IOA/meta_theory/Seq.thy	Tue Jan 09 15:36:30 2001 +0100
    19.3 @@ -36,7 +36,7 @@
    19.4     "Finite"     :: "'a seq => bool"
    19.5  
    19.6  translations
    19.7 -   "xs @@ ys" == "sconc`xs`ys"
    19.8 +   "xs @@ ys" == "sconc$xs$ys"
    19.9     "Finite x" == "x:sfinite"
   19.10     "~(Finite x)" =="x~:sfinite"
   19.11  
   19.12 @@ -47,63 +47,63 @@
   19.13  (* f not possible at lhs, as "pattern matching" only for % x arguments,
   19.14     f cannot be written at rhs in front, as fix_eq3 does not apply later *)
   19.15  smap_def
   19.16 -  "smap == (fix`(LAM h f tr. case tr of 
   19.17 +  "smap == (fix$(LAM h f tr. case tr of 
   19.18        nil   => nil
   19.19 -    | x##xs => f`x ## h`f`xs))"
   19.20 +    | x##xs => f$x ## h$f$xs))"
   19.21  
   19.22  sfilter_def       
   19.23 -  "sfilter == (fix`(LAM h P t. case t of 
   19.24 +  "sfilter == (fix$(LAM h P t. case t of 
   19.25  	   nil => nil
   19.26 -	 | x##xs => If P`x                                 
   19.27 -                    then x##(h`P`xs)
   19.28 -                    else     h`P`xs
   19.29 +	 | x##xs => If P$x                                 
   19.30 +                    then x##(h$P$xs)
   19.31 +                    else     h$P$xs
   19.32                      fi))" 
   19.33  sforall_def
   19.34 -  "sforall P t == (sforall2`P`t ~=FF)" 
   19.35 +  "sforall P t == (sforall2$P$t ~=FF)" 
   19.36  
   19.37  
   19.38  sforall2_def
   19.39 -  "sforall2 == (fix`(LAM h P t. case t of 
   19.40 +  "sforall2 == (fix$(LAM h P t. case t of 
   19.41  	   nil => TT
   19.42 -	 | x##xs => P`x andalso h`P`xs))"
   19.43 +	 | x##xs => P$x andalso h$P$xs))"
   19.44    
   19.45  sconc_def
   19.46 -  "sconc == (fix`(LAM h t1 t2. case t1 of 
   19.47 +  "sconc == (fix$(LAM h t1 t2. case t1 of 
   19.48                 nil       => t2
   19.49 -             | x##xs => x##(h`xs`t2)))"
   19.50 +             | x##xs => x##(h$xs$t2)))"
   19.51  
   19.52  slast_def
   19.53 -  "slast == (fix`(LAM h t. case t of 
   19.54 +  "slast == (fix$(LAM h t. case t of 
   19.55  	   nil => UU
   19.56 -	 | x##xs => (If is_nil`xs                              
   19.57 +	 | x##xs => (If is_nil$xs                              
   19.58                            then x
   19.59 -                         else h`xs fi)))"
   19.60 +                         else h$xs fi)))"
   19.61  
   19.62  stakewhile_def      
   19.63 -  "stakewhile == (fix`(LAM h P t. case t of 
   19.64 +  "stakewhile == (fix$(LAM h P t. case t of 
   19.65  	   nil => nil
   19.66 -	 | x##xs => If P`x                                 
   19.67 -                    then x##(h`P`xs)
   19.68 +	 | x##xs => If P$x                                 
   19.69 +                    then x##(h$P$xs)
   19.70                      else nil
   19.71                      fi))" 
   19.72  sdropwhile_def
   19.73 -  "sdropwhile == (fix`(LAM h P t. case t of 
   19.74 +  "sdropwhile == (fix$(LAM h P t. case t of 
   19.75  	   nil => nil
   19.76 -	 | x##xs => If P`x                                 
   19.77 -                    then h`P`xs
   19.78 +	 | x##xs => If P$x                                 
   19.79 +                    then h$P$xs
   19.80                      else t
   19.81                      fi))" 
   19.82  sflat_def
   19.83 -  "sflat == (fix`(LAM h t. case t of 
   19.84 +  "sflat == (fix$(LAM h t. case t of 
   19.85  	   nil => nil
   19.86 -	 | x##xs => x @@ (h`xs)))"
   19.87 +	 | x##xs => x @@ (h$xs)))"
   19.88  
   19.89  szip_def
   19.90 -  "szip == (fix`(LAM h t1 t2. case t1 of 
   19.91 +  "szip == (fix$(LAM h t1 t2. case t1 of 
   19.92                 nil   => nil
   19.93               | x##xs => (case t2 of 
   19.94                            nil => UU 
   19.95 -                        | y##ys => <x,y>##(h`xs`ys))))"
   19.96 +                        | y##ys => <x,y>##(h$xs$ys))))"
   19.97  
   19.98  Partial_def
   19.99    "Partial x  == (seq_finite x) & ~(Finite x)"
    20.1 --- a/src/HOLCF/IOA/meta_theory/Sequence.ML	Tue Jan 09 15:32:27 2001 +0100
    20.2 +++ b/src/HOLCF/IOA/meta_theory/Sequence.ML	Tue Jan 09 15:36:30 2001 +0100
    20.3 @@ -18,15 +18,15 @@
    20.4  (*                               Map                                *)
    20.5  (* ---------------------------------------------------------------- *)
    20.6  
    20.7 -Goal "Map f`UU =UU";
    20.8 +Goal "Map f$UU =UU";
    20.9  by (simp_tac (simpset() addsimps [Map_def]) 1);
   20.10  qed"Map_UU";
   20.11  
   20.12 -Goal "Map f`nil =nil";
   20.13 +Goal "Map f$nil =nil";
   20.14  by (simp_tac (simpset() addsimps [Map_def]) 1);
   20.15  qed"Map_nil";
   20.16  
   20.17 -Goal "Map f`(x>>xs)=(f x) >> Map f`xs";
   20.18 +Goal "Map f$(x>>xs)=(f x) >> Map f$xs";
   20.19  by (simp_tac (simpset() addsimps [Map_def, Consq_def,flift2_def]) 1);
   20.20  qed"Map_cons";
   20.21  
   20.22 @@ -34,15 +34,15 @@
   20.23  (*                               Filter                             *)
   20.24  (* ---------------------------------------------------------------- *)
   20.25  
   20.26 -Goal "Filter P`UU =UU";
   20.27 +Goal "Filter P$UU =UU";
   20.28  by (simp_tac (simpset() addsimps [Filter_def]) 1);
   20.29  qed"Filter_UU";
   20.30  
   20.31 -Goal "Filter P`nil =nil";
   20.32 +Goal "Filter P$nil =nil";
   20.33  by (simp_tac (simpset() addsimps [Filter_def]) 1);
   20.34  qed"Filter_nil";
   20.35  
   20.36 -Goal "Filter P`(x>>xs)= (if P x then x>>(Filter P`xs) else Filter P`xs)"; 
   20.37 +Goal "Filter P$(x>>xs)= (if P x then x>>(Filter P$xs) else Filter P$xs)"; 
   20.38  by (simp_tac (simpset() addsimps [Filter_def, Consq_def,flift2_def,If_and_if]) 1);
   20.39  qed"Filter_cons";
   20.40  
   20.41 @@ -76,15 +76,15 @@
   20.42  (*                               Takewhile                          *)
   20.43  (* ---------------------------------------------------------------- *)
   20.44  
   20.45 -Goal "Takewhile P`UU =UU";
   20.46 +Goal "Takewhile P$UU =UU";
   20.47  by (simp_tac (simpset() addsimps [Takewhile_def]) 1);
   20.48  qed"Takewhile_UU";
   20.49  
   20.50 -Goal "Takewhile P`nil =nil";
   20.51 +Goal "Takewhile P$nil =nil";
   20.52  by (simp_tac (simpset() addsimps [Takewhile_def]) 1);
   20.53  qed"Takewhile_nil";
   20.54  
   20.55 -Goal "Takewhile P`(x>>xs)= (if P x then x>>(Takewhile P`xs) else nil)"; 
   20.56 +Goal "Takewhile P$(x>>xs)= (if P x then x>>(Takewhile P$xs) else nil)"; 
   20.57  by (simp_tac (simpset() addsimps [Takewhile_def, Consq_def,flift2_def,If_and_if]) 1);
   20.58  qed"Takewhile_cons";
   20.59  
   20.60 @@ -92,15 +92,15 @@
   20.61  (*                               Dropwhile                          *)
   20.62  (* ---------------------------------------------------------------- *)
   20.63  
   20.64 -Goal "Dropwhile P`UU =UU";
   20.65 +Goal "Dropwhile P$UU =UU";
   20.66  by (simp_tac (simpset() addsimps [Dropwhile_def]) 1);
   20.67  qed"Dropwhile_UU";
   20.68  
   20.69 -Goal "Dropwhile P`nil =nil";
   20.70 +Goal "Dropwhile P$nil =nil";
   20.71  by (simp_tac (simpset() addsimps [Dropwhile_def]) 1);
   20.72  qed"Dropwhile_nil";
   20.73  
   20.74 -Goal "Dropwhile P`(x>>xs)= (if P x then Dropwhile P`xs else x>>xs)"; 
   20.75 +Goal "Dropwhile P$(x>>xs)= (if P x then Dropwhile P$xs else x>>xs)"; 
   20.76  by (simp_tac (simpset() addsimps [Dropwhile_def, Consq_def,flift2_def,If_and_if]) 1);
   20.77  qed"Dropwhile_cons";
   20.78  
   20.79 @@ -109,15 +109,15 @@
   20.80  (* ---------------------------------------------------------------- *)
   20.81  
   20.82  
   20.83 -Goal "Last`UU =UU";
   20.84 +Goal "Last$UU =UU";
   20.85  by (simp_tac (simpset() addsimps [Last_def]) 1);
   20.86  qed"Last_UU";
   20.87  
   20.88 -Goal "Last`nil =UU";
   20.89 +Goal "Last$nil =UU";
   20.90  by (simp_tac (simpset() addsimps [Last_def]) 1);
   20.91  qed"Last_nil";
   20.92  
   20.93 -Goal "Last`(x>>xs)= (if xs=nil then Def x else Last`xs)"; 
   20.94 +Goal "Last$(x>>xs)= (if xs=nil then Def x else Last$xs)"; 
   20.95  by (simp_tac (simpset() addsimps [Last_def, Consq_def]) 1);
   20.96  by (res_inst_tac [("x","xs")] seq.casedist 1);
   20.97  by (Asm_simp_tac 1);
   20.98 @@ -129,15 +129,15 @@
   20.99  (*                               Flat                               *)
  20.100  (* ---------------------------------------------------------------- *)
  20.101  
  20.102 -Goal "Flat`UU =UU";
  20.103 +Goal "Flat$UU =UU";
  20.104  by (simp_tac (simpset() addsimps [Flat_def]) 1);
  20.105  qed"Flat_UU";
  20.106  
  20.107 -Goal "Flat`nil =nil";
  20.108 +Goal "Flat$nil =nil";
  20.109  by (simp_tac (simpset() addsimps [Flat_def]) 1);
  20.110  qed"Flat_nil";
  20.111  
  20.112 -Goal "Flat`(x##xs)= x @@ (Flat`xs)"; 
  20.113 +Goal "Flat$(x##xs)= x @@ (Flat$xs)"; 
  20.114  by (simp_tac (simpset() addsimps [Flat_def, Consq_def]) 1);
  20.115  qed"Flat_cons";
  20.116  
  20.117 @@ -154,7 +154,7 @@
  20.118  \                                      Undef  => UU \
  20.119  \                                    | Def a => (case y of \
  20.120  \                                                  Undef => UU \
  20.121 -\                                                | Def b => Def (a,b)##(Zip`xs`ys)))))";
  20.122 +\                                                | Def b => Def (a,b)##(Zip$xs$ys)))))";
  20.123  by (rtac trans 1);
  20.124  by (rtac fix_eq2 1);
  20.125  by (rtac Zip_def 1);
  20.126 @@ -162,29 +162,29 @@
  20.127  by (Simp_tac 1);
  20.128  qed"Zip_unfold";
  20.129  
  20.130 -Goal "Zip`UU`y =UU";
  20.131 +Goal "Zip$UU$y =UU";
  20.132  by (stac Zip_unfold 1);
  20.133  by (Simp_tac 1);
  20.134  qed"Zip_UU1";
  20.135  
  20.136 -Goal "x~=nil ==> Zip`x`UU =UU";
  20.137 +Goal "x~=nil ==> Zip$x$UU =UU";
  20.138  by (stac Zip_unfold 1);
  20.139  by (Simp_tac 1);
  20.140  by (res_inst_tac [("x","x")] seq.casedist 1);
  20.141  by (REPEAT (Asm_full_simp_tac 1));
  20.142  qed"Zip_UU2";
  20.143  
  20.144 -Goal "Zip`nil`y =nil";
  20.145 +Goal "Zip$nil$y =nil";
  20.146  by (stac Zip_unfold 1);
  20.147  by (Simp_tac 1);
  20.148  qed"Zip_nil";
  20.149  
  20.150 -Goal "Zip`(x>>xs)`nil= UU"; 
  20.151 +Goal "Zip$(x>>xs)$nil= UU"; 
  20.152  by (stac Zip_unfold 1);
  20.153  by (simp_tac (simpset() addsimps [Consq_def]) 1);
  20.154  qed"Zip_cons_nil";
  20.155  
  20.156 -Goal "Zip`(x>>xs)`(y>>ys)= (x,y) >> Zip`xs`ys"; 
  20.157 +Goal "Zip$(x>>xs)$(y>>ys)= (x,y) >> Zip$xs$ys"; 
  20.158  by (rtac trans 1);
  20.159  by (stac Zip_unfold 1);
  20.160  by (Simp_tac 1);
  20.161 @@ -298,7 +298,7 @@
  20.162  by (etac monofun_cfun_arg 1);
  20.163  qed"Cons_inject_less_eq";
  20.164  
  20.165 -Goal "seq_take (Suc n)`(a>>x) = a>> (seq_take n`x)";
  20.166 +Goal "seq_take (Suc n)$(a>>x) = a>> (seq_take n$x)";
  20.167  by (simp_tac (simpset() addsimps [Consq_def]) 1);
  20.168  qed"seq_take_Cons";
  20.169  
  20.170 @@ -365,11 +365,11 @@
  20.171  
  20.172  section "HD,TL";
  20.173  
  20.174 -Goal "HD`(x>>y) = Def x";
  20.175 +Goal "HD$(x>>y) = Def x";
  20.176  by (simp_tac (simpset() addsimps [Consq_def]) 1);
  20.177  qed"HD_Cons";
  20.178  
  20.179 -Goal "TL`(x>>y) = y";
  20.180 +Goal "TL$(x>>y) = y";
  20.181  by (simp_tac (simpset() addsimps [Consq_def]) 1);
  20.182  qed"TL_Cons";
  20.183  
  20.184 @@ -415,11 +415,11 @@
  20.185  Addsimps [FiniteConc];
  20.186  
  20.187  
  20.188 -Goal "Finite s ==> Finite (Map f`s)";
  20.189 +Goal "Finite s ==> Finite (Map f$s)";
  20.190  by (Seq_Finite_induct_tac 1);
  20.191  qed"FiniteMap1";
  20.192  
  20.193 -Goal "Finite s ==> ! t. (s = Map f`t) --> Finite t";
  20.194 +Goal "Finite s ==> ! t. (s = Map f$t) --> Finite t";
  20.195  by (Seq_Finite_induct_tac 1);
  20.196  by (strip_tac 1);
  20.197  by (Seq_case_simp_tac "t" 1);
  20.198 @@ -430,7 +430,7 @@
  20.199  by (Asm_full_simp_tac 1);
  20.200  qed"FiniteMap2";
  20.201  
  20.202 -Goal "Finite (Map f`s) = Finite s";
  20.203 +Goal "Finite (Map f$s) = Finite s";
  20.204  by Auto_tac;
  20.205  by (etac (FiniteMap2 RS spec RS mp) 1);
  20.206  by (rtac refl 1);
  20.207 @@ -438,7 +438,7 @@
  20.208  qed"Map2Finite";
  20.209  
  20.210  
  20.211 -Goal "Finite s ==> Finite (Filter P`s)";
  20.212 +Goal "Finite s ==> Finite (Filter P$s)";
  20.213  by (Seq_Finite_induct_tac 1);
  20.214  qed"FiniteFilter";
  20.215  
  20.216 @@ -519,11 +519,11 @@
  20.217  
  20.218  section "Last";
  20.219  
  20.220 -Goal "Finite s ==> s~=nil --> Last`s~=UU";
  20.221 +Goal "Finite s ==> s~=nil --> Last$s~=UU";
  20.222  by (Seq_Finite_induct_tac  1);
  20.223  qed"Finite_Last1";
  20.224  
  20.225 -Goal "Finite s ==> Last`s=UU --> s=nil";
  20.226 +Goal "Finite s ==> Last$s=UU --> s=nil";
  20.227  by (Seq_Finite_induct_tac  1);
  20.228  by (fast_tac HOL_cs 1);
  20.229  qed"Finite_Last2";
  20.230 @@ -535,11 +535,11 @@
  20.231  section "Filter, Conc";
  20.232  
  20.233  
  20.234 -Goal "Filter P`(Filter Q`s) = Filter (%x. P x & Q x)`s";
  20.235 +Goal "Filter P$(Filter Q$s) = Filter (%x. P x & Q x)$s";
  20.236  by (Seq_induct_tac "s" [Filter_def] 1);
  20.237  qed"FilterPQ";
  20.238  
  20.239 -Goal "Filter P`(x @@ y) = (Filter P`x @@ Filter P`y)";
  20.240 +Goal "Filter P$(x @@ y) = (Filter P$x @@ Filter P$y)";
  20.241  by (simp_tac (simpset() addsimps [Filter_def,sfiltersconc]) 1);
  20.242  qed"FilterConc";
  20.243  
  20.244 @@ -547,24 +547,24 @@
  20.245  
  20.246  section "Map";
  20.247  
  20.248 -Goal "Map f`(Map g`s) = Map (f o g)`s";
  20.249 +Goal "Map f$(Map g$s) = Map (f o g)$s";
  20.250  by (Seq_induct_tac "s" [] 1);
  20.251  qed"MapMap";
  20.252  
  20.253 -Goal "Map f`(x@@y) = (Map f`x) @@ (Map f`y)";
  20.254 +Goal "Map f$(x@@y) = (Map f$x) @@ (Map f$y)";
  20.255  by (Seq_induct_tac "x" [] 1);
  20.256  qed"MapConc";
  20.257  
  20.258 -Goal "Filter P`(Map f`x) = Map f`(Filter (P o f)`x)";
  20.259 +Goal "Filter P$(Map f$x) = Map f$(Filter (P o f)$x)";
  20.260  by (Seq_induct_tac "x" [] 1);
  20.261  qed"MapFilter";
  20.262  
  20.263 -Goal "nil = (Map f`s) --> s= nil";
  20.264 +Goal "nil = (Map f$s) --> s= nil";
  20.265  by (Seq_case_simp_tac "s" 1);
  20.266  qed"nilMap";
  20.267  
  20.268  
  20.269 -Goal "Forall P (Map f`s) = Forall (P o f) s";
  20.270 +Goal "Forall P (Map f$s) = Forall (P o f) s";
  20.271  by (Seq_induct_tac "s" [Forall_def,sforall_def] 1);
  20.272  qed"ForallMap";
  20.273  
  20.274 @@ -593,13 +593,13 @@
  20.275  
  20.276  Addsimps [Forall_Conc];
  20.277  
  20.278 -Goal "Forall P s  --> Forall P (TL`s)";
  20.279 +Goal "Forall P s  --> Forall P (TL$s)";
  20.280  by (Seq_induct_tac "s" [Forall_def,sforall_def] 1);
  20.281  qed"ForallTL1";
  20.282  
  20.283  bind_thm ("ForallTL",ForallTL1 RS mp);
  20.284  
  20.285 -Goal "Forall P s  --> Forall P (Dropwhile Q`s)";
  20.286 +Goal "Forall P s  --> Forall P (Dropwhile Q$s)";
  20.287  by (Seq_induct_tac "s" [Forall_def,sforall_def] 1);
  20.288  qed"ForallDropwhile1";
  20.289  
  20.290 @@ -624,7 +624,7 @@
  20.291  qed"Forall_postfixclosed";
  20.292  
  20.293  
  20.294 -Goal "((! x. P x --> (Q x = R x)) & Forall P tr) --> Filter Q`tr = Filter R`tr";
  20.295 +Goal "((! x. P x --> (Q x = R x)) & Forall P tr) --> Filter Q$tr = Filter R$tr";
  20.296  by (Seq_induct_tac "tr" [Forall_def,sforall_def] 1);
  20.297  qed"ForallPFilterQR1";
  20.298  
  20.299 @@ -636,12 +636,12 @@
  20.300  section "Forall, Filter";
  20.301  
  20.302  
  20.303 -Goal "Forall P (Filter P`x)";
  20.304 +Goal "Forall P (Filter P$x)";
  20.305  by (simp_tac (simpset() addsimps [Filter_def,Forall_def,forallPsfilterP]) 1);
  20.306  qed"ForallPFilterP";
  20.307  
  20.308  (* holds also in other direction, then equal to forallPfilterP *)
  20.309 -Goal "Forall P x --> Filter P`x = x";
  20.310 +Goal "Forall P x --> Filter P$x = x";
  20.311  by (Seq_induct_tac "x" [Forall_def,sforall_def,Filter_def] 1);
  20.312  qed"ForallPFilterPid1";
  20.313  
  20.314 @@ -650,7 +650,7 @@
  20.315  
  20.316  (* holds also in other direction *)
  20.317  Goal "!! ys . Finite ys ==> \
  20.318 -\   Forall (%x. ~P x) ys --> Filter P`ys = nil ";
  20.319 +\   Forall (%x. ~P x) ys --> Filter P$ys = nil ";
  20.320  by (Seq_Finite_induct_tac 1);
  20.321  qed"ForallnPFilterPnil1";
  20.322  
  20.323 @@ -659,7 +659,7 @@
  20.324  
  20.325  (* holds also in other direction *)
  20.326  Goal   "~Finite ys & Forall (%x. ~P x) ys \
  20.327 -\                  --> Filter P`ys = UU ";
  20.328 +\                  --> Filter P$ys = UU ";
  20.329  by (Seq_induct_tac "ys" [Forall_def,sforall_def] 1);
  20.330  qed"ForallnPFilterPUU1";
  20.331  
  20.332 @@ -668,7 +668,7 @@
  20.333  
  20.334  (* inverse of ForallnPFilterPnil *)
  20.335  
  20.336 -Goal "!! ys . Filter P`ys = nil --> \
  20.337 +Goal "!! ys . Filter P$ys = nil --> \
  20.338  \   (Forall (%x. ~P x) ys & Finite ys)";
  20.339  by (res_inst_tac[("x","ys")] Seq_induct 1);
  20.340  (* adm *)
  20.341 @@ -685,15 +685,15 @@
  20.342  
  20.343  (* inverse of ForallnPFilterPUU. proved by 2 lemmas because of adm problems *)
  20.344  
  20.345 -Goal "Finite ys ==> Filter P`ys ~= UU";
  20.346 +Goal "Finite ys ==> Filter P$ys ~= UU";
  20.347  by (Seq_Finite_induct_tac 1);
  20.348  qed"FilterUU_nFinite_lemma1";
  20.349  
  20.350 -Goal "~ Forall (%x. ~P x) ys --> Filter P`ys ~= UU";
  20.351 +Goal "~ Forall (%x. ~P x) ys --> Filter P$ys ~= UU";
  20.352  by (Seq_induct_tac "ys" [Forall_def,sforall_def] 1);
  20.353  qed"FilterUU_nFinite_lemma2";
  20.354  
  20.355 -Goal   "Filter P`ys = UU ==> \
  20.356 +Goal   "Filter P$ys = UU ==> \
  20.357  \                (Forall (%x. ~P x) ys  & ~Finite ys)";
  20.358  by (rtac conjI 1);
  20.359  by (cut_inst_tac [] (FilterUU_nFinite_lemma2 RS mp COMP rev_contrapos) 1);
  20.360 @@ -703,14 +703,14 @@
  20.361  
  20.362  
  20.363  Goal  "!! Q P.[| Forall Q ys; Finite ys; !!x. Q x ==> ~P x|] \
  20.364 -\   ==> Filter P`ys = nil";
  20.365 +\   ==> Filter P$ys = nil";
  20.366  by (etac ForallnPFilterPnil 1);
  20.367  by (etac ForallPForallQ 1);
  20.368  by Auto_tac;
  20.369  qed"ForallQFilterPnil";
  20.370  
  20.371  Goal "!! Q P. [| ~Finite ys; Forall Q ys;  !!x. Q x ==> ~P x|] \
  20.372 -\   ==> Filter P`ys = UU ";
  20.373 +\   ==> Filter P$ys = UU ";
  20.374  by (etac ForallnPFilterPUU 1);
  20.375  by (etac ForallPForallQ 1);
  20.376  by Auto_tac;
  20.377 @@ -723,20 +723,20 @@
  20.378  section "Takewhile, Forall, Filter";
  20.379  
  20.380  
  20.381 -Goal "Forall P (Takewhile P`x)";
  20.382 +Goal "Forall P (Takewhile P$x)";
  20.383  by (simp_tac (simpset() addsimps [Forall_def,Takewhile_def,sforallPstakewhileP]) 1);
  20.384  qed"ForallPTakewhileP";
  20.385  
  20.386  
  20.387 -Goal"!! P. [| !!x. Q x==> P x |] ==> Forall P (Takewhile Q`x)";
  20.388 +Goal"!! P. [| !!x. Q x==> P x |] ==> Forall P (Takewhile Q$x)";
  20.389  by (rtac ForallPForallQ 1);
  20.390  by (rtac ForallPTakewhileP 1);
  20.391  by Auto_tac;
  20.392  qed"ForallPTakewhileQ";
  20.393  
  20.394  
  20.395 -Goal  "!! Q P.[| Finite (Takewhile Q`ys); !!x. Q x ==> ~P x |] \
  20.396 -\   ==> Filter P`(Takewhile Q`ys) = nil";
  20.397 +Goal  "!! Q P.[| Finite (Takewhile Q$ys); !!x. Q x ==> ~P x |] \
  20.398 +\   ==> Filter P$(Takewhile Q$ys) = nil";
  20.399  by (etac ForallnPFilterPnil 1);
  20.400  by (rtac ForallPForallQ 1);
  20.401  by (rtac ForallPTakewhileP 1);
  20.402 @@ -744,7 +744,7 @@
  20.403  qed"FilterPTakewhileQnil";
  20.404  
  20.405  Goal "!! Q P. [| !!x. Q x ==> P x |] ==> \
  20.406 -\            Filter P`(Takewhile Q`ys) = (Takewhile Q`ys)";
  20.407 +\            Filter P$(Takewhile Q$ys) = (Takewhile Q$ys)";
  20.408  by (rtac ForallPFilterPid 1);
  20.409  by (rtac ForallPForallQ 1);
  20.410  by (rtac ForallPTakewhileP 1);
  20.411 @@ -754,28 +754,28 @@
  20.412  Addsimps [ForallPTakewhileP,ForallPTakewhileQ,
  20.413            FilterPTakewhileQnil,FilterPTakewhileQid];
  20.414  
  20.415 -Goal "Takewhile P`(Takewhile P`s) = Takewhile P`s";
  20.416 +Goal "Takewhile P$(Takewhile P$s) = Takewhile P$s";
  20.417  by (Seq_induct_tac "s" [Forall_def,sforall_def] 1);
  20.418  qed"Takewhile_idempotent";
  20.419  
  20.420 -Goal "Forall P s --> Takewhile (%x. Q x | (~P x))`s = Takewhile Q`s";
  20.421 +Goal "Forall P s --> Takewhile (%x. Q x | (~P x))$s = Takewhile Q$s";
  20.422  by (Seq_induct_tac "s" [Forall_def,sforall_def] 1);
  20.423  qed"ForallPTakewhileQnP";
  20.424  
  20.425 -Goal "Forall P s --> Dropwhile (%x. Q x | (~P x))`s = Dropwhile Q`s";
  20.426 +Goal "Forall P s --> Dropwhile (%x. Q x | (~P x))$s = Dropwhile Q$s";
  20.427  by (Seq_induct_tac "s" [Forall_def,sforall_def] 1);
  20.428  qed"ForallPDropwhileQnP";
  20.429  
  20.430  Addsimps [ForallPTakewhileQnP RS mp, ForallPDropwhileQnP RS mp];
  20.431  
  20.432  
  20.433 -Goal "Forall P s --> Takewhile P`(s @@ t) = s @@ (Takewhile P`t)";
  20.434 +Goal "Forall P s --> Takewhile P$(s @@ t) = s @@ (Takewhile P$t)";
  20.435  by (Seq_induct_tac "s" [Forall_def,sforall_def] 1);
  20.436  qed"TakewhileConc1";
  20.437  
  20.438  bind_thm("TakewhileConc",TakewhileConc1 RS mp);
  20.439  
  20.440 -Goal "Finite s ==> Forall P s --> Dropwhile P`(s @@ t) = Dropwhile P`t";
  20.441 +Goal "Finite s ==> Forall P s --> Dropwhile P$(s @@ t) = Dropwhile P$t";
  20.442  by (Seq_Finite_induct_tac 1);
  20.443  qed"DropwhileConc1";
  20.444  
  20.445 @@ -788,9 +788,9 @@
  20.446  section "coinductive characterizations of Filter";
  20.447  
  20.448  
  20.449 -Goal "HD`(Filter P`y) = Def x \
  20.450 -\         --> y = ((Takewhile (%x. ~P x)`y) @@ (x >> TL`(Dropwhile (%a.~P a)`y)))  \
  20.451 -\             & Finite (Takewhile (%x. ~ P x)`y)  & P x";
  20.452 +Goal "HD$(Filter P$y) = Def x \
  20.453 +\         --> y = ((Takewhile (%x. ~P x)$y) @@ (x >> TL$(Dropwhile (%a.~P a)$y)))  \
  20.454 +\             & Finite (Takewhile (%x. ~ P x)$y)  & P x";
  20.455  
  20.456  (* FIX: pay attention: is only admissible with chain-finite package to be added to 
  20.457          adm test and Finite f x admissibility *)
  20.458 @@ -804,16 +804,16 @@
  20.459  by (Asm_full_simp_tac 1); 
  20.460  qed"divide_Seq_lemma";
  20.461  
  20.462 -Goal "(x>>xs) << Filter P`y  \
  20.463 -\   ==> y = ((Takewhile (%a. ~ P a)`y) @@ (x >> TL`(Dropwhile (%a.~P a)`y))) \
  20.464 -\      & Finite (Takewhile (%a. ~ P a)`y)  & P x";
  20.465 +Goal "(x>>xs) << Filter P$y  \
  20.466 +\   ==> y = ((Takewhile (%a. ~ P a)$y) @@ (x >> TL$(Dropwhile (%a.~P a)$y))) \
  20.467 +\      & Finite (Takewhile (%a. ~ P a)$y)  & P x";
  20.468  by (rtac (divide_Seq_lemma RS mp) 1);
  20.469  by (dres_inst_tac [("fo","HD"),("xa","x>>xs")]  monofun_cfun_arg 1);
  20.470  by (Asm_full_simp_tac 1); 
  20.471  qed"divide_Seq";
  20.472  
  20.473   
  20.474 -Goal "~Forall P y --> (? x. HD`(Filter (%a. ~P a)`y) = Def x)";
  20.475 +Goal "~Forall P y --> (? x. HD$(Filter (%a. ~P a)$y) = Def x)";
  20.476  (* Pay attention: is only admissible with chain-finite package to be added to 
  20.477          adm test *)
  20.478  by (Seq_induct_tac "y" [Forall_def,sforall_def] 1);
  20.479 @@ -821,8 +821,8 @@
  20.480  
  20.481  
  20.482  Goal "~Forall P y  \
  20.483 -\  ==> ? x. y= (Takewhile P`y @@ (x >> TL`(Dropwhile P`y))) & \
  20.484 -\      Finite (Takewhile P`y) & (~ P x)";
  20.485 +\  ==> ? x. y= (Takewhile P$y @@ (x >> TL$(Dropwhile P$y))) & \
  20.486 +\      Finite (Takewhile P$y) & (~ P x)";
  20.487  by (dtac (nForall_HDFilter RS mp) 1);
  20.488  by (safe_tac set_cs);
  20.489  by (res_inst_tac [("x","x")] exI 1);
  20.490 @@ -846,15 +846,15 @@
  20.491  
  20.492  section "take_lemma";
  20.493  
  20.494 -Goal "(!n. seq_take n`x = seq_take n`x') = (x = x')";
  20.495 +Goal "(!n. seq_take n$x = seq_take n$x') = (x = x')";
  20.496  by (rtac iffI 1);
  20.497  by (resolve_tac seq.take_lemmas 1);
  20.498  by Auto_tac;
  20.499  qed"seq_take_lemma";
  20.500  
  20.501  Goal 
  20.502 -"  ! n. ((! k. k < n --> seq_take k`y1 = seq_take k`y2) \
  20.503 -\   --> seq_take n`(x @@ (t>>y1)) =  seq_take n`(x @@ (t>>y2)))";
  20.504 +"  ! n. ((! k. k < n --> seq_take k$y1 = seq_take k$y2) \
  20.505 +\   --> seq_take n$(x @@ (t>>y1)) =  seq_take n$(x @@ (t>>y2)))";
  20.506  by (Seq_induct_tac "x" [] 1);
  20.507  by (strip_tac 1);
  20.508  by (case_tac "n" 1);
  20.509 @@ -864,8 +864,8 @@
  20.510  qed"take_reduction1";
  20.511  
  20.512  
  20.513 -Goal "!! n.[| x=y; s=t; !! k. k<n ==> seq_take k`y1 = seq_take k`y2|] \
  20.514 -\ ==> seq_take n`(x @@ (s>>y1)) =  seq_take n`(y @@ (t>>y2))";
  20.515 +Goal "!! n.[| x=y; s=t; !! k. k<n ==> seq_take k$y1 = seq_take k$y2|] \
  20.516 +\ ==> seq_take n$(x @@ (s>>y1)) =  seq_take n$(y @@ (t>>y2))";
  20.517  
  20.518  by (auto_tac (claset() addSIs [take_reduction1 RS spec RS mp],simpset()));
  20.519  qed"take_reduction";
  20.520 @@ -875,8 +875,8 @@
  20.521     ------------------------------------------------------------------ *)
  20.522  
  20.523  Goal 
  20.524 -"  ! n. ((! k. k < n --> seq_take k`y1 << seq_take k`y2) \
  20.525 -\   --> seq_take n`(x @@ (t>>y1)) <<  seq_take n`(x @@ (t>>y2)))";
  20.526 +"  ! n. ((! k. k < n --> seq_take k$y1 << seq_take k$y2) \
  20.527 +\   --> seq_take n$(x @@ (t>>y1)) <<  seq_take n$(x @@ (t>>y2)))";
  20.528  by (Seq_induct_tac "x" [] 1);
  20.529  by (strip_tac 1);
  20.530  by (case_tac "n" 1);
  20.531 @@ -886,14 +886,14 @@
  20.532  qed"take_reduction_less1";
  20.533  
  20.534  
  20.535 -Goal "!! n.[| x=y; s=t;!! k. k<n ==> seq_take k`y1 << seq_take k`y2|] \
  20.536 -\ ==> seq_take n`(x @@ (s>>y1)) <<  seq_take n`(y @@ (t>>y2))";
  20.537 +Goal "!! n.[| x=y; s=t;!! k. k<n ==> seq_take k$y1 << seq_take k$y2|] \
  20.538 +\ ==> seq_take n$(x @@ (s>>y1)) <<  seq_take n$(y @@ (t>>y2))";
  20.539  by (auto_tac (claset() addSIs [take_reduction_less1 RS spec RS mp],simpset()));
  20.540  qed"take_reduction_less";
  20.541  
  20.542  
  20.543  val prems = goalw thy [seq.take_def]
  20.544 -"(!! n. seq_take n`s1 << seq_take n`s2)  ==> s1<<s2";
  20.545 +"(!! n. seq_take n$s1 << seq_take n$s2)  ==> s1<<s2";
  20.546  
  20.547  by (res_inst_tac [("t","s1")] (seq.reach RS subst)  1);
  20.548  by (res_inst_tac [("t","s2")] (seq.reach RS subst)  1);
  20.549 @@ -910,7 +910,7 @@
  20.550  qed"take_lemma_less1";
  20.551  
  20.552  
  20.553 -Goal "(!n. seq_take n`x << seq_take n`x') = (x << x')";
  20.554 +Goal "(!n. seq_take n$x << seq_take n$x') = (x << x')";
  20.555  by (rtac iffI 1);
  20.556  by (rtac take_lemma_less1 1);
  20.557  by Auto_tac;
  20.558 @@ -931,8 +931,8 @@
  20.559  
  20.560  Goal "!! Q. [|!! s. [| Forall Q s; A s |] ==> (f s) = (g s) ; \
  20.561  \           !! s1 s2 y. [| Forall Q s1; Finite s1; ~ Q y; A (s1 @@ y>>s2)|] \
  20.562 -\                         ==> ! n. seq_take n`(f (s1 @@ y>>s2)) \
  20.563 -\                                = seq_take n`(g (s1 @@ y>>s2)) |] \
  20.564 +\                         ==> ! n. seq_take n$(f (s1 @@ y>>s2)) \
  20.565 +\                                = seq_take n$(g (s1 @@ y>>s2)) |] \
  20.566  \              ==> A x --> (f x)=(g x)";
  20.567  by (case_tac "Forall Q x" 1);
  20.568  by (auto_tac (claset() addSDs [divide_Seq3],simpset()));
  20.569 @@ -951,10 +951,10 @@
  20.570  
  20.571  Goal 
  20.572  "!! Q. [|!! s. [| Forall Q s; A s |] ==> (f s) = (g s) ; \
  20.573 -\        !! s1 s2 y n. [| ! t. A t --> seq_take n`(f t) = seq_take n`(g t);\
  20.574 +\        !! s1 s2 y n. [| ! t. A t --> seq_take n$(f t) = seq_take n$(g t);\
  20.575  \                         Forall Q s1; Finite s1; ~ Q y; A (s1 @@ y>>s2) |] \
  20.576 -\                         ==>   seq_take (Suc n)`(f (s1 @@ y>>s2)) \
  20.577 -\                             = seq_take (Suc n)`(g (s1 @@ y>>s2)) |] \
  20.578 +\                         ==>   seq_take (Suc n)$(f (s1 @@ y>>s2)) \
  20.579 +\                             = seq_take (Suc n)$(g (s1 @@ y>>s2)) |] \
  20.580  \              ==> A x --> (f x)=(g x)";
  20.581  by (rtac impI 1);
  20.582  by (resolve_tac seq.take_lemmas 1);
  20.583 @@ -973,10 +973,10 @@
  20.584  
  20.585  Goal 
  20.586  "!! Q. [|!! s. [| Forall Q s; A s |] ==> (f s) = (g s) ; \
  20.587 -\        !! s1 s2 y n. [| ! t m. m < n --> A t --> seq_take m`(f t) = seq_take m`(g t);\
  20.588 +\        !! s1 s2 y n. [| ! t m. m < n --> A t --> seq_take m$(f t) = seq_take m$(g t);\
  20.589  \                         Forall Q s1; Finite s1; ~ Q y; A (s1 @@ y>>s2) |] \
  20.590 -\                         ==>   seq_take n`(f (s1 @@ y>>s2)) \
  20.591 -\                             = seq_take n`(g (s1 @@ y>>s2)) |] \
  20.592 +\                         ==>   seq_take n$(f (s1 @@ y>>s2)) \
  20.593 +\                             = seq_take n$(g (s1 @@ y>>s2)) |] \
  20.594  \              ==> A x --> (f x)=(g x)";
  20.595  by (rtac impI 1);
  20.596  by (resolve_tac seq.take_lemmas 1);
  20.597 @@ -1025,10 +1025,10 @@
  20.598  
  20.599  Goal 
  20.600  "!! Q. [|!! s h1 h2. [| Forall Q s; A s h1 h2|] ==> (f s h1 h2) = (g s h1 h2) ; \
  20.601 -\  !! 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);\
  20.602 +\  !! 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);\
  20.603  \                         Forall Q s1; Finite s1; ~ Q y; A (s1 @@ y>>s2) h1 h2|] \
  20.604 -\                         ==>   seq_take n`(f (s1 @@ y>>s2) h1 h2) \
  20.605 -\                             = seq_take n`(g (s1 @@ y>>s2) h1 h2) |] \
  20.606 +\                         ==>   seq_take n$(f (s1 @@ y>>s2) h1 h2) \
  20.607 +\                             = seq_take n$(g (s1 @@ y>>s2) h1 h2) |] \
  20.608  \              ==> ! h1 h2. (A x h1 h2) --> (f x h1 h2)=(g x h1 h2)";
  20.609  by (strip_tac 1);
  20.610  by (resolve_tac seq.take_lemmas 1);
  20.611 @@ -1049,14 +1049,14 @@
  20.612  
  20.613  Goal 
  20.614  "!! Q. [|!! s. Forall Q s ==> P ((f s) = (g s)) ; \
  20.615 -\        !! s1 s2 y n. [| ! t m. m < n --> P (seq_take m`(f t) = seq_take m`(g t));\
  20.616 +\        !! s1 s2 y n. [| ! t m. m < n --> P (seq_take m$(f t) = seq_take m$(g t));\
  20.617  \                         Forall Q s1; Finite s1; ~ Q y|] \
  20.618 -\                         ==>   P (seq_take n`(f (s1 @@ y>>s2)) \
  20.619 -\                                   = seq_take n`(g (s1 @@ y>>s2))) |] \
  20.620 +\                         ==>   P (seq_take n$(f (s1 @@ y>>s2)) \
  20.621 +\                                   = seq_take n$(g (s1 @@ y>>s2))) |] \
  20.622  \              ==> P ((f x)=(g x))";
  20.623  
  20.624  by (res_inst_tac [("t","f x = g x"),
  20.625 -                  ("s","!n. seq_take n`(f x) = seq_take n`(g x)")] subst 1);
  20.626 +                  ("s","!n. seq_take n$(f x) = seq_take n$(g x)")] subst 1);
  20.627  by (rtac seq_take_lemma 1);
  20.628  
  20.629  wie ziehe ich n durch P, d.h. evtl. ns in P muessen umbenannt werden.....
  20.630 @@ -1079,10 +1079,10 @@
  20.631  Goal 
  20.632  "!! Q. [| A UU  ==> (f UU) = (g UU) ; \
  20.633  \         A nil ==> (f nil) = (g nil) ; \
  20.634 -\         !! s y n. [| ! t. A t --> seq_take n`(f t) = seq_take n`(g t);\
  20.635 +\         !! s y n. [| ! t. A t --> seq_take n$(f t) = seq_take n$(g t);\
  20.636  \                    A (y>>s) |]   \
  20.637 -\                    ==>   seq_take (Suc n)`(f (y>>s)) \
  20.638 -\                        = seq_take (Suc n)`(g (y>>s)) |] \
  20.639 +\                    ==>   seq_take (Suc n)$(f (y>>s)) \
  20.640 +\                        = seq_take (Suc n)$(g (y>>s)) |] \
  20.641  \              ==> A x --> (f x)=(g x)";
  20.642  by (rtac impI 1);
  20.643  by (resolve_tac seq.take_lemmas 1);
  20.644 @@ -1111,26 +1111,26 @@
  20.645  (* In general: How to do this case without the same adm problems 
  20.646     as for the entire proof ? *) 
  20.647  Goal "Forall (%x.~(P x & Q x)) s \
  20.648 -\         --> Filter P`(Filter Q`s) =\
  20.649 -\             Filter (%x. P x & Q x)`s";
  20.650 +\         --> Filter P$(Filter Q$s) =\
  20.651 +\             Filter (%x. P x & Q x)$s";
  20.652  
  20.653  by (Seq_induct_tac "s" [Forall_def,sforall_def] 1);
  20.654  qed"Filter_lemma1";
  20.655  
  20.656  Goal "Finite s ==>  \
  20.657  \         (Forall (%x. (~P x) | (~ Q x)) s  \
  20.658 -\         --> Filter P`(Filter Q`s) = nil)";
  20.659 +\         --> Filter P$(Filter Q$s) = nil)";
  20.660  by (Seq_Finite_induct_tac 1);
  20.661  qed"Filter_lemma2";
  20.662  
  20.663  Goal "Finite s ==>  \
  20.664  \         Forall (%x. (~P x) | (~ Q x)) s  \
  20.665 -\         --> Filter (%x. P x & Q x)`s = nil";
  20.666 +\         --> Filter (%x. P x & Q x)$s = nil";
  20.667  by (Seq_Finite_induct_tac 1);
  20.668  qed"Filter_lemma3";
  20.669  
  20.670  
  20.671 -Goal "Filter P`(Filter Q`s) = Filter (%x. P x & Q x)`s";
  20.672 +Goal "Filter P$(Filter Q$s) = Filter (%x. P x & Q x)$s";
  20.673  by (res_inst_tac [("A1","%x. True") 
  20.674                   ,("Q1","%x.~(P x & Q x)"),("x1","s")]
  20.675                   (take_lemma_induct RS mp) 1);
  20.676 @@ -1149,7 +1149,7 @@
  20.677  
  20.678  
  20.679  
  20.680 -Goal "Map f`(x@@y) = (Map f`x) @@ (Map f`y)";
  20.681 +Goal "Map f$(x@@y) = (Map f$x) @@ (Map f$y)";
  20.682  by (res_inst_tac [("A1","%x. True"), ("x1","x")]
  20.683      (take_lemma_in_eq_out RS mp) 1);
  20.684  by Auto_tac;
    21.1 --- a/src/HOLCF/IOA/meta_theory/Sequence.thy	Tue Jan 09 15:32:27 2001 +0100
    21.2 +++ b/src/HOLCF/IOA/meta_theory/Sequence.thy	Tue Jan 09 15:36:30 2001 +0100
    21.3 @@ -42,7 +42,7 @@
    21.4  
    21.5  translations
    21.6  
    21.7 -  "a>>s"         == "Consq a`s"
    21.8 +  "a>>s"         == "Consq a$s"
    21.9    "[x, xs!]"     == "x>>[xs!]"
   21.10    "[x!]"         == "x>>nil"
   21.11    "[x, xs?]"     == "x>>[xs?]"
   21.12 @@ -53,22 +53,22 @@
   21.13  
   21.14  Consq_def     "Consq a == LAM s. Def a ## s"
   21.15  
   21.16 -Filter_def    "Filter P == sfilter`(flift2 P)"
   21.17 +Filter_def    "Filter P == sfilter$(flift2 P)"
   21.18  
   21.19 -Map_def       "Map f  == smap`(flift2 f)"
   21.20 +Map_def       "Map f  == smap$(flift2 f)"
   21.21  
   21.22  Forall_def    "Forall P == sforall (flift2 P)"
   21.23  
   21.24  Last_def      "Last == slast"
   21.25  
   21.26 -Dropwhile_def "Dropwhile P == sdropwhile`(flift2 P)"
   21.27 +Dropwhile_def "Dropwhile P == sdropwhile$(flift2 P)"
   21.28  
   21.29 -Takewhile_def "Takewhile P == stakewhile`(flift2 P)"
   21.30 +Takewhile_def "Takewhile P == stakewhile$(flift2 P)"
   21.31  
   21.32  Flat_def      "Flat == sflat"
   21.33  
   21.34  Zip_def
   21.35 -  "Zip == (fix`(LAM h t1 t2. case t1 of 
   21.36 +  "Zip == (fix$(LAM h t1 t2. case t1 of 
   21.37                 nil   => nil
   21.38               | x##xs => (case t2 of 
   21.39                            nil => UU 
   21.40 @@ -76,13 +76,13 @@
   21.41                                        Undef  => UU
   21.42                                      | Def a => (case y of 
   21.43                                                    Undef => UU
   21.44 -                                                | Def b => Def (a,b)##(h`xs`ys))))))"
   21.45 +                                                | Def b => Def (a,b)##(h$xs$ys))))))"
   21.46  
   21.47 -Filter2_def    "Filter2 P == (fix`(LAM h t. case t of 
   21.48 +Filter2_def    "Filter2 P == (fix$(LAM h t. case t of 
   21.49              nil => nil
   21.50  	  | x##xs => (case x of Undef => UU | Def y => (if P y                                 
   21.51 -                     then x##(h`xs)
   21.52 -                     else     h`xs))))" 
   21.53 +                     then x##(h$xs)
   21.54 +                     else     h$xs))))" 
   21.55  
   21.56  rules
   21.57  
    22.1 --- a/src/HOLCF/IOA/meta_theory/ShortExecutions.ML	Tue Jan 09 15:32:27 2001 +0100
    22.2 +++ b/src/HOLCF/IOA/meta_theory/ShortExecutions.ML	Tue Jan 09 15:36:30 2001 +0100
    22.3 @@ -29,24 +29,24 @@
    22.4  \    | x##xs => \
    22.5  \      (case x of\ 
    22.6  \        Undef => UU\
    22.7 -\      | Def y => (Takewhile (%a.~ P a)`s)\
    22.8 -\                  @@ (y>>(oraclebuild P`(TL`(Dropwhile (%a.~ P a)`s))`xs))\
    22.9 +\      | Def y => (Takewhile (%a.~ P a)$s)\
   22.10 +\                  @@ (y>>(oraclebuild P$(TL$(Dropwhile (%a.~ P a)$s))$xs))\
   22.11  \      )\
   22.12  \    )");
   22.13  
   22.14 -Goal "oraclebuild P`sch`UU = UU";
   22.15 +Goal "oraclebuild P$sch$UU = UU";
   22.16  by (stac oraclebuild_unfold 1);
   22.17  by (Simp_tac 1);
   22.18  qed"oraclebuild_UU";
   22.19  
   22.20 -Goal "oraclebuild P`sch`nil = nil";
   22.21 +Goal "oraclebuild P$sch$nil = nil";
   22.22  by (stac oraclebuild_unfold 1);
   22.23  by (Simp_tac 1);
   22.24  qed"oraclebuild_nil";
   22.25  
   22.26 -Goal "oraclebuild P`s`(x>>t) = \
   22.27 -\         (Takewhile (%a.~ P a)`s)   \
   22.28 -\          @@ (x>>(oraclebuild P`(TL`(Dropwhile (%a.~ P a)`s))`t))";     
   22.29 +Goal "oraclebuild P$s$(x>>t) = \
   22.30 +\         (Takewhile (%a.~ P a)$s)   \
   22.31 +\          @@ (x>>(oraclebuild P$(TL$(Dropwhile (%a.~ P a)$s))$t))";     
   22.32  by (rtac trans 1);
   22.33  by (stac oraclebuild_unfold 1);
   22.34  by (asm_full_simp_tac (simpset() addsimps [Consq_def]) 1);
   22.35 @@ -63,7 +63,7 @@
   22.36  Goalw [Cut_def]
   22.37  "[| Forall (%a.~ P a) s; Finite s|] \
   22.38  \           ==> Cut P s =nil";
   22.39 -by (subgoal_tac "Filter P`s = nil" 1);
   22.40 +by (subgoal_tac "Filter P$s = nil" 1);
   22.41  by (asm_simp_tac (simpset() addsimps [oraclebuild_nil]) 1);
   22.42  by (rtac ForallQFilterPnil 1);
   22.43  by (REPEAT (atac 1));
   22.44 @@ -72,7 +72,7 @@
   22.45  Goalw [Cut_def]
   22.46  "[| Forall (%a.~ P a) s; ~Finite s|] \
   22.47  \           ==> Cut P s =UU";
   22.48 -by (subgoal_tac "Filter P`s= UU" 1);
   22.49 +by (subgoal_tac "Filter P$s= UU" 1);
   22.50  by (asm_simp_tac (simpset() addsimps [oraclebuild_UU]) 1);
   22.51  by (rtac ForallQFilterPUU 1);
   22.52  by (REPEAT (atac 1));
   22.53 @@ -93,7 +93,7 @@
   22.54  (* ---------------------------------------------------------------- *)
   22.55  
   22.56  
   22.57 -Goal "Filter P`s = Filter P`(Cut P s)";
   22.58 +Goal "Filter P$s = Filter P$(Cut P s)";
   22.59  
   22.60  by (res_inst_tac [("A1","%x. True")
   22.61                   ,("Q1","%x.~ P x"), ("x1","s")]
   22.62 @@ -128,7 +128,7 @@
   22.63  qed"Cut_idemp";
   22.64  
   22.65  
   22.66 -Goal "Map f`(Cut (P o f) s) = Cut P (Map f`s)";
   22.67 +Goal "Map f$(Cut (P o f) s) = Cut P (Map f$s)";
   22.68  
   22.69  by (res_inst_tac [("A1","%x. True")
   22.70                   ,("Q1","%x.~ P (f x)"), ("x1","s")]
   22.71 @@ -200,13 +200,13 @@
   22.72  
   22.73  
   22.74  Goalw [schedules_def,has_schedule_def]
   22.75 - "[|sch : schedules A ; tr = Filter (%a. a:ext A)`sch|] \
   22.76 + "[|sch : schedules A ; tr = Filter (%a. a:ext A)$sch|] \
   22.77  \   ==> ? sch. sch : schedules A & \
   22.78 -\              tr = Filter (%a. a:ext A)`sch &\
   22.79 +\              tr = Filter (%a. a:ext A)$sch &\
   22.80  \              LastActExtsch A sch";
   22.81  
   22.82  by (safe_tac set_cs);
   22.83 -by (res_inst_tac [("x","filter_act`(Cut (%a. fst a:ext A) (snd ex))")] exI 1);
   22.84 +by (res_inst_tac [("x","filter_act$(Cut (%a. fst a:ext A) (snd ex))")] exI 1);
   22.85  by (asm_full_simp_tac (simpset() addsimps [executions_def]) 1);
   22.86  by (pair_tac "ex" 1);
   22.87  by (safe_tac set_cs);
   22.88 @@ -220,7 +220,7 @@
   22.89  (* Subgoal 2:  Lemma:  Filter P s = Filter P (Cut P s) *)
   22.90  
   22.91  by (simp_tac (simpset() addsimps [filter_act_def]) 1);
   22.92 -by (subgoal_tac "Map fst`(Cut (%a. fst a: ext A) y)= Cut (%a. a:ext A) (Map fst`y)" 1);
   22.93 +by (subgoal_tac "Map fst$(Cut (%a. fst a: ext A) y)= Cut (%a. a:ext A) (Map fst$y)" 1);
   22.94  
   22.95  by (rtac (rewrite_rule [o_def] MapCut) 2);
   22.96  by (asm_full_simp_tac (simpset() addsimps [FilterCut RS sym]) 1);
   22.97 @@ -228,7 +228,7 @@
   22.98  (* Subgoal 3: Lemma: Cut idempotent  *)
   22.99  
  22.100  by (simp_tac (simpset() addsimps [LastActExtsch_def,filter_act_def]) 1);
  22.101 -by (subgoal_tac "Map fst`(Cut (%a. fst a: ext A) y)= Cut (%a. a:ext A) (Map fst`y)" 1);
  22.102 +by (subgoal_tac "Map fst$(Cut (%a. fst a: ext A) y)= Cut (%a. a:ext A) (Map fst$y)" 1);
  22.103  by (rtac (rewrite_rule [o_def] MapCut) 2);
  22.104  by (asm_full_simp_tac (simpset() addsimps [Cut_idemp]) 1);
  22.105  qed"exists_LastActExtsch";
  22.106 @@ -239,7 +239,7 @@
  22.107  (* ---------------------------------------------------------------- *)
  22.108  
  22.109  Goalw [LastActExtsch_def]
  22.110 -  "[| LastActExtsch A sch; Filter (%x. x:ext A)`sch = nil |] \
  22.111 +  "[| LastActExtsch A sch; Filter (%x. x:ext A)$sch = nil |] \
  22.112  \   ==> sch=nil";
  22.113  by (dtac FilternPnilForallP 1);
  22.114  by (etac conjE 1);
  22.115 @@ -249,7 +249,7 @@
  22.116  qed"LastActExtimplnil";
  22.117  
  22.118  Goalw [LastActExtsch_def]
  22.119 -  "[| LastActExtsch A sch; Filter (%x. x:ext A)`sch = UU |] \
  22.120 +  "[| LastActExtsch A sch; Filter (%x. x:ext A)$sch = UU |] \
  22.121  \   ==> sch=UU";
  22.122  by (dtac FilternPUUForallP 1);
  22.123  by (etac conjE 1);
    23.1 --- a/src/HOLCF/IOA/meta_theory/ShortExecutions.thy	Tue Jan 09 15:32:27 2001 +0100
    23.2 +++ b/src/HOLCF/IOA/meta_theory/ShortExecutions.thy	Tue Jan 09 15:36:30 2001 +0100
    23.3 @@ -28,19 +28,19 @@
    23.4    "LastActExtsch A sch == (Cut (%x. x: ext A) sch = sch)"
    23.5  
    23.6  (* LastActExtex_def
    23.7 -  "LastActExtex A ex == LastActExtsch A (filter_act`ex)" *)
    23.8 +  "LastActExtex A ex == LastActExtsch A (filter_act$ex)" *)
    23.9  
   23.10  Cut_def
   23.11 -  "Cut P s == oraclebuild P`s`(Filter P`s)"
   23.12 +  "Cut P s == oraclebuild P$s$(Filter P$s)"
   23.13  
   23.14  oraclebuild_def
   23.15 -  "oraclebuild P == (fix`(LAM h s t. case t of 
   23.16 +  "oraclebuild P == (fix$(LAM h s t. case t of 
   23.17         nil => nil
   23.18      | x##xs => 
   23.19        (case x of 
   23.20          Undef => UU
   23.21 -      | Def y => (Takewhile (%x.~P x)`s)
   23.22 -                  @@ (y>>(h`(TL`(Dropwhile (%x.~ P x)`s))`xs))
   23.23 +      | Def y => (Takewhile (%x.~P x)$s)
   23.24 +                  @@ (y>>(h$(TL$(Dropwhile (%x.~ P x)$s))$xs))
   23.25        )
   23.26      ))"
   23.27  
   23.28 @@ -53,7 +53,7 @@
   23.29    "Finite s ==> (? y. s = Cut P s @@ y)"
   23.30  
   23.31  LastActExtsmall1
   23.32 -  "LastActExtsch A sch ==> LastActExtsch A (TL`(Dropwhile P`sch))"
   23.33 +  "LastActExtsch A sch ==> LastActExtsch A (TL$(Dropwhile P$sch))"
   23.34  
   23.35  LastActExtsmall2
   23.36    "[| Finite sch1; LastActExtsch A (sch1 @@ sch2) |] ==> LastActExtsch A sch2"
    24.1 --- a/src/HOLCF/IOA/meta_theory/SimCorrectness.ML	Tue Jan 09 15:32:27 2001 +0100
    24.2 +++ b/src/HOLCF/IOA/meta_theory/SimCorrectness.ML	Tue Jan 09 15:36:30 2001 +0100
    24.3 @@ -24,8 +24,8 @@
    24.4  \                                 T' = @t'. ? ex1. (t,t'):R & move A ex1 s a t' \
    24.5  \                             in \
    24.6  \                                (@cex. move A cex s a T')  \
    24.7 -\                              @@ ((corresp_ex_simC A R `xs) T'))   \
    24.8 -\                        `x) ))";
    24.9 +\                              @@ ((corresp_ex_simC A R $xs) T'))   \
   24.10 +\                        $x) ))";
   24.11  by (rtac trans 1);
   24.12  by (rtac fix_eq2 1);
   24.13  by (rtac corresp_ex_simC_def 1);
   24.14 @@ -33,21 +33,21 @@
   24.15  by (simp_tac (simpset() addsimps [flift1_def]) 1);
   24.16  qed"corresp_ex_simC_unfold";
   24.17  
   24.18 -Goal "(corresp_ex_simC A R`UU) s=UU";
   24.19 +Goal "(corresp_ex_simC A R$UU) s=UU";
   24.20  by (stac corresp_ex_simC_unfold 1);
   24.21  by (Simp_tac 1);
   24.22  qed"corresp_ex_simC_UU";
   24.23  
   24.24 -Goal "(corresp_ex_simC A R`nil) s = nil";
   24.25 +Goal "(corresp_ex_simC A R$nil) s = nil";
   24.26  by (stac corresp_ex_simC_unfold 1);
   24.27  by (Simp_tac 1);
   24.28  qed"corresp_ex_simC_nil";
   24.29  
   24.30 -Goal "(corresp_ex_simC A R`((a,t)>>xs)) s = \
   24.31 +Goal "(corresp_ex_simC A R$((a,t)>>xs)) s = \
   24.32  \          (let T' = @t'. ? ex1. (t,t'):R & move A ex1 s a t' \
   24.33  \           in  \
   24.34  \            (@cex. move A cex s a T')  \ 
   24.35 -\             @@ ((corresp_ex_simC A R`xs) T'))";
   24.36 +\             @@ ((corresp_ex_simC A R$xs) T'))";
   24.37  by (rtac trans 1);
   24.38  by (stac corresp_ex_simC_unfold 1);
   24.39  by (asm_full_simp_tac (simpset() addsimps [Consq_def,flift1_def]) 1);
   24.40 @@ -128,7 +128,7 @@
   24.41  Goal
   24.42     "[|is_simulation R C A; reachable C s; s-a--C-> t; (s,s'):R|] ==>\
   24.43  \   let T' = @t'. ? ex1. (t,t'):R & move A ex1 s' a t' in \
   24.44 -\     mk_trace A`((@x. move A x s' a T')) = \
   24.45 +\     mk_trace A$((@x. move A x s' a T')) = \
   24.46  \       (if a:ext A then a>>nil else nil)";
   24.47  by (cut_inst_tac [] move_is_move_sim 1);
   24.48  by (REPEAT (assume_tac 1));
   24.49 @@ -160,7 +160,7 @@
   24.50  Goal 
   24.51    "[|is_simulation R C A; ext C = ext A|] ==>  \     
   24.52  \        !s s'. reachable C s & is_exec_frag C (s,ex) & (s,s'): R --> \
   24.53 -\            mk_trace C`ex = mk_trace A`((corresp_ex_simC A R`ex) s')";
   24.54 +\            mk_trace C$ex = mk_trace A$((corresp_ex_simC A R$ex) s')";
   24.55  
   24.56  by (pair_induct_tac "ex" [is_exec_frag_def] 1);
   24.57  (* cons case *) 
   24.58 @@ -190,7 +190,7 @@
   24.59  Goal 
   24.60   "[| is_simulation R C A |] ==>\
   24.61  \ !s s'. reachable C s & is_exec_frag C (s,ex) & (s,s'):R  \
   24.62 -\ --> is_exec_frag A (s',(corresp_ex_simC A R`ex) s')"; 
   24.63 +\ --> is_exec_frag A (s',(corresp_ex_simC A R$ex) s')"; 
   24.64  
   24.65  by (Asm_full_simp_tac 1);
   24.66  by (pair_induct_tac "ex" [is_exec_frag_def] 1);
    25.1 --- a/src/HOLCF/IOA/meta_theory/SimCorrectness.thy	Tue Jan 09 15:32:27 2001 +0100
    25.2 +++ b/src/HOLCF/IOA/meta_theory/SimCorrectness.thy	Tue Jan 09 15:36:30 2001 +0100
    25.3 @@ -23,17 +23,17 @@
    25.4  corresp_ex_sim_def
    25.5    "corresp_ex_sim A R ex == let S'= (@s'.(fst ex,s'):R & s': starts_of A)
    25.6                              in 
    25.7 -                               (S',(corresp_ex_simC A R`(snd ex)) S')"
    25.8 +                               (S',(corresp_ex_simC A R$(snd ex)) S')"
    25.9  
   25.10  
   25.11  corresp_ex_simC_def
   25.12 -  "corresp_ex_simC A R  == (fix`(LAM h ex. (%s. case ex of 
   25.13 +  "corresp_ex_simC A R  == (fix$(LAM h ex. (%s. case ex of 
   25.14        nil =>  nil
   25.15      | x##xs => (flift1 (%pr. let a = (fst pr); t = (snd pr);
   25.16                                   T' = @t'. ? ex1. (t,t'):R & move A ex1 s a t' 
   25.17                               in
   25.18                                  (@cex. move A cex s a T')
   25.19 -                                 @@ ((h`xs) T'))
   25.20 -                        `x) )))"
   25.21 +                                 @@ ((h$xs) T'))
   25.22 +                        $x) )))"
   25.23   
   25.24  end
   25.25 \ No newline at end of file
    26.1 --- a/src/HOLCF/IOA/meta_theory/Simulations.ML	Tue Jan 09 15:32:27 2001 +0100
    26.2 +++ b/src/HOLCF/IOA/meta_theory/Simulations.ML	Tue Jan 09 15:36:30 2001 +0100
    26.3 @@ -19,7 +19,7 @@
    26.4  
    26.5  
    26.6  Goalw [Image_def]
    26.7 -"(R```{x} Int S ~= {}) = (? y. (x,y):R & y:S)";
    26.8 +"(R``{x} Int S ~= {}) = (? y. (x,y):R & y:S)";
    26.9  by (simp_tac (simpset() addsimps [Int_non_empty]) 1);
   26.10  qed"Sim_start_convert";
   26.11  
    27.1 --- a/src/HOLCF/IOA/meta_theory/Simulations.thy	Tue Jan 09 15:32:27 2001 +0100
    27.2 +++ b/src/HOLCF/IOA/meta_theory/Simulations.thy	Tue Jan 09 15:36:30 2001 +0100
    27.3 @@ -23,7 +23,7 @@
    27.4  
    27.5  is_simulation_def
    27.6    "is_simulation R C A ==                          
    27.7 -   (!s:starts_of C. R```{s} Int starts_of A ~= {}) &        
    27.8 +   (!s:starts_of C. R``{s} Int starts_of A ~= {}) &        
    27.9     (!s s' t a. reachable C s &                      
   27.10                 s -a--C-> t   &
   27.11                 (s,s') : R              
   27.12 @@ -31,7 +31,7 @@
   27.13  
   27.14  is_backward_simulation_def
   27.15    "is_backward_simulation R C A ==                          
   27.16 -   (!s:starts_of C. R```{s} <= starts_of A) &        
   27.17 +   (!s:starts_of C. R``{s} <= starts_of A) &        
   27.18     (!s t t' a. reachable C s &                      
   27.19                 s -a--C-> t   &
   27.20                 (t,t') : R              
    28.1 --- a/src/HOLCF/IOA/meta_theory/TL.ML	Tue Jan 09 15:32:27 2001 +0100
    28.2 +++ b/src/HOLCF/IOA/meta_theory/TL.ML	Tue Jan 09 15:36:30 2001 +0100
    28.3 @@ -106,7 +106,7 @@
    28.4  
    28.5  
    28.6  Goalw [tsuffix_def,suffix_def]
    28.7 -"s~=UU & s~=nil --> tsuffix s2 (TL`s) --> tsuffix s2 s";
    28.8 +"s~=UU & s~=nil --> tsuffix s2 (TL$s) --> tsuffix s2 s";
    28.9  by Auto_tac;
   28.10  by (Seq_case_simp_tac "s" 1);
   28.11  by (res_inst_tac [("x","a>>s1")] exI 1);
    29.1 --- a/src/HOLCF/IOA/meta_theory/TL.thy	Tue Jan 09 15:32:27 2001 +0100
    29.2 +++ b/src/HOLCF/IOA/meta_theory/TL.thy	Tue Jan 09 15:36:30 2001 +0100
    29.3 @@ -50,7 +50,7 @@
    29.4  
    29.5  (* this means that for nil and UU the effect is unpredictable *)
    29.6  Init_def
    29.7 -  "Init P s ==  (P (unlift (HD`s)))" 
    29.8 +  "Init P s ==  (P (unlift (HD$s)))" 
    29.9  
   29.10  suffix_def
   29.11    "suffix s2 s == ? s1. (Finite s1  & s = s1 @@ s2)" 
   29.12 @@ -62,7 +62,7 @@
   29.13    "([] P) s == ! s2. tsuffix s2 s --> P s2"
   29.14  
   29.15  Next_def
   29.16 -  "(Next P) s == if (TL`s=UU | TL`s=nil) then (P s) else P (TL`s)"
   29.17 +  "(Next P) s == if (TL$s=UU | TL$s=nil) then (P s) else P (TL$s)"
   29.18  
   29.19  Diamond_def
   29.20    "<> P == .~ ([] (.~ P))"
    30.1 --- a/src/HOLCF/IOA/meta_theory/TLS.ML	Tue Jan 09 15:32:27 2001 +0100
    30.2 +++ b/src/HOLCF/IOA/meta_theory/TLS.ML	Tue Jan 09 15:36:30 2001 +0100
    30.3 @@ -20,8 +20,8 @@
    30.4  Goal "ex2seqC  = (LAM ex. (%s. case ex of \
    30.5  \      nil =>  (s,None,s)>>nil   \
    30.6  \    | x##xs => (flift1 (%pr. \
    30.7 -\                (s,Some (fst pr), snd pr)>> (ex2seqC`xs) (snd pr))  \
    30.8 -\                `x)  \
    30.9 +\                (s,Some (fst pr), snd pr)>> (ex2seqC$xs) (snd pr))  \
   30.10 +\                $x)  \
   30.11  \      ))";
   30.12  by (rtac trans 1);
   30.13  by (rtac fix_eq2 1);
   30.14 @@ -30,18 +30,18 @@
   30.15  by (simp_tac (simpset() addsimps [flift1_def]) 1);
   30.16  qed"ex2seqC_unfold";
   30.17  
   30.18 -Goal "(ex2seqC `UU) s=UU";
   30.19 +Goal "(ex2seqC $UU) s=UU";
   30.20  by (stac ex2seqC_unfold 1);
   30.21  by (Simp_tac 1);
   30.22  qed"ex2seqC_UU";
   30.23  
   30.24 -Goal "(ex2seqC `nil) s = (s,None,s)>>nil";
   30.25 +Goal "(ex2seqC $nil) s = (s,None,s)>>nil";
   30.26  by (stac ex2seqC_unfold 1);
   30.27  by (Simp_tac 1);
   30.28  qed"ex2seqC_nil";
   30.29  
   30.30 -Goal "(ex2seqC `((a,t)>>xs)) s = \
   30.31 -\          (s,Some a,t)>> ((ex2seqC`xs) t)";
   30.32 +Goal "(ex2seqC $((a,t)>>xs)) s = \
   30.33 +\          (s,Some a,t)>> ((ex2seqC$xs) t)";
   30.34  by (rtac trans 1);
   30.35  by (stac ex2seqC_unfold 1);
   30.36  by (asm_full_simp_tac (simpset() addsimps [Consq_def,flift1_def]) 1);
    31.1 --- a/src/HOLCF/IOA/meta_theory/TLS.thy	Tue Jan 09 15:32:27 2001 +0100
    31.2 +++ b/src/HOLCF/IOA/meta_theory/TLS.thy	Tue Jan 09 15:36:30 2001 +0100
    31.3 @@ -60,14 +60,14 @@
    31.4    "xt2 P tr == P (fst (snd tr))"
    31.5  
    31.6  ex2seq_def
    31.7 -  "ex2seq ex == ((ex2seqC `(mkfin (snd ex))) (fst ex))"
    31.8 +  "ex2seq ex == ((ex2seqC $(mkfin (snd ex))) (fst ex))"
    31.9  
   31.10  ex2seqC_def
   31.11 -  "ex2seqC == (fix`(LAM h ex. (%s. case ex of 
   31.12 +  "ex2seqC == (fix$(LAM h ex. (%s. case ex of 
   31.13        nil =>  (s,None,s)>>nil
   31.14      | x##xs => (flift1 (%pr.
   31.15 -                (s,Some (fst pr), snd pr)>> (h`xs) (snd pr)) 
   31.16 -                `x)
   31.17 +                (s,Some (fst pr), snd pr)>> (h$xs) (snd pr)) 
   31.18 +                $x)
   31.19        )))"
   31.20  
   31.21  validTE_def
    32.1 --- a/src/HOLCF/IOA/meta_theory/Traces.ML	Tue Jan 09 15:32:27 2001 +0100
    32.2 +++ b/src/HOLCF/IOA/meta_theory/Traces.ML	Tue Jan 09 15:36:30 2001 +0100
    32.3 @@ -26,15 +26,15 @@
    32.4  (* ---------------------------------------------------------------- *)
    32.5  
    32.6  
    32.7 -Goal  "filter_act`UU = UU";
    32.8 +Goal  "filter_act$UU = UU";
    32.9  by (simp_tac (simpset() addsimps [filter_act_def]) 1);
   32.10  qed"filter_act_UU";
   32.11  
   32.12 -Goal  "filter_act`nil = nil";
   32.13 +Goal  "filter_act$nil = nil";
   32.14  by (simp_tac (simpset() addsimps [filter_act_def]) 1);
   32.15  qed"filter_act_nil";
   32.16  
   32.17 -Goal "filter_act`(x>>xs) = (fst x) >> filter_act`xs";
   32.18 +Goal "filter_act$(x>>xs) = (fst x) >> filter_act$xs";
   32.19  by (simp_tac (simpset() addsimps [filter_act_def]) 1);
   32.20  qed"filter_act_cons";
   32.21  
   32.22 @@ -45,18 +45,18 @@
   32.23  (*                             mk_trace                             *)
   32.24  (* ---------------------------------------------------------------- *)
   32.25  
   32.26 -Goal "mk_trace A`UU=UU";
   32.27 +Goal "mk_trace A$UU=UU";
   32.28  by (simp_tac (simpset() addsimps [mk_trace_def]) 1);
   32.29  qed"mk_trace_UU";
   32.30  
   32.31 -Goal "mk_trace A`nil=nil";
   32.32 +Goal "mk_trace A$nil=nil";
   32.33  by (simp_tac (simpset() addsimps [mk_trace_def]) 1);
   32.34  qed"mk_trace_nil";
   32.35  
   32.36 -Goal "mk_trace A`(at >> xs) =    \
   32.37 +Goal "mk_trace A$(at >> xs) =    \
   32.38  \            (if ((fst at):ext A)    \       
   32.39 -\                 then (fst at) >> (mk_trace A`xs) \   
   32.40 -\                 else mk_trace A`xs)";
   32.41 +\                 then (fst at) >> (mk_trace A$xs) \   
   32.42 +\                 else mk_trace A$xs)";
   32.43  
   32.44  by (asm_full_simp_tac (simpset() addsimps [mk_trace_def]) 1);
   32.45  qed"mk_trace_cons";
   32.46 @@ -71,8 +71,8 @@
   32.47  Goal "is_exec_fragC A = (LAM ex. (%s. case ex of \
   32.48  \      nil => TT \
   32.49  \    | x##xs => (flift1 \ 
   32.50 -\            (%p. Def ((s,p):trans_of A) andalso (is_exec_fragC A`xs) (snd p)) \
   32.51 -\             `x) \
   32.52 +\            (%p. Def ((s,p):trans_of A) andalso (is_exec_fragC A$xs) (snd p)) \
   32.53 +\             $x) \
   32.54  \   ))";
   32.55  by (rtac trans 1);
   32.56  by (rtac fix_eq2 1);
   32.57 @@ -81,19 +81,19 @@
   32.58  by (simp_tac (simpset() addsimps [flift1_def]) 1);
   32.59  qed"is_exec_fragC_unfold";
   32.60  
   32.61 -Goal "(is_exec_fragC A`UU) s=UU";
   32.62 +Goal "(is_exec_fragC A$UU) s=UU";
   32.63  by (stac is_exec_fragC_unfold 1);
   32.64  by (Simp_tac 1);
   32.65  qed"is_exec_fragC_UU";
   32.66  
   32.67 -Goal "(is_exec_fragC A`nil) s = TT";
   32.68 +Goal "(is_exec_fragC A$nil) s = TT";
   32.69  by (stac is_exec_fragC_unfold 1);
   32.70  by (Simp_tac 1);
   32.71  qed"is_exec_fragC_nil";
   32.72  
   32.73 -Goal "(is_exec_fragC A`(pr>>xs)) s = \
   32.74 +Goal "(is_exec_fragC A$(pr>>xs)) s = \
   32.75  \                        (Def ((s,pr):trans_of A) \
   32.76 -\                andalso (is_exec_fragC A`xs)(snd pr))";
   32.77 +\                andalso (is_exec_fragC A$xs)(snd pr))";
   32.78  by (rtac trans 1);
   32.79  by (stac is_exec_fragC_unfold 1);
   32.80  by (asm_full_simp_tac (simpset() addsimps [Consq_def,flift1_def]) 1);
   32.81 @@ -163,7 +163,7 @@
   32.82     take the detour of schedules *)
   32.83  
   32.84  Goalw  [executions_def,mk_trace_def,has_trace_def,schedules_def,has_schedule_def] 
   32.85 -"has_trace A b = (? ex:executions A. b = mk_trace A`(snd ex))";
   32.86 +"has_trace A b = (? ex:executions A. b = mk_trace A$(snd ex))";
   32.87  
   32.88  by (safe_tac set_cs);
   32.89  (* 1 *)
   32.90 @@ -173,7 +173,7 @@
   32.91  by (Simp_tac 1);
   32.92  by (Asm_simp_tac 1);
   32.93  (* 2 *)
   32.94 -by (res_inst_tac[("x","filter_act`(snd ex)")] bexI 1);
   32.95 +by (res_inst_tac[("x","filter_act$(snd ex)")] bexI 1);
   32.96  by (stac beta_cfun 1);
   32.97  by (cont_tacR 1);
   32.98  by (Simp_tac 1);
   32.99 @@ -195,7 +195,7 @@
  32.100  
  32.101  Goal 
  32.102    "!! A. is_trans_of A ==> \
  32.103 -\ ! s. is_exec_frag A (s,xs) --> Forall (%a. a:act A) (filter_act`xs)";
  32.104 +\ ! s. is_exec_frag A (s,xs) --> Forall (%a. a:act A) (filter_act$xs)";
  32.105  
  32.106  by (pair_induct_tac "xs" [is_exec_frag_def,Forall_def,sforall_def] 1);
  32.107  (* main case *)
  32.108 @@ -206,7 +206,7 @@
  32.109  
  32.110  Goal 
  32.111    "!! A.[|  is_trans_of A; x:executions A |] ==> \
  32.112 -\ Forall (%a. a:act A) (filter_act`(snd x))";
  32.113 +\ Forall (%a. a:act A) (filter_act$(snd x))";
  32.114  
  32.115  by (asm_full_simp_tac (simpset() addsimps [executions_def]) 1);
  32.116  by (pair_tac "x" 1);
    33.1 --- a/src/HOLCF/IOA/meta_theory/Traces.thy	Tue Jan 09 15:32:27 2001 +0100
    33.2 +++ b/src/HOLCF/IOA/meta_theory/Traces.thy	Tue Jan 09 15:36:30 2001 +0100
    33.3 @@ -74,15 +74,15 @@
    33.4  
    33.5  
    33.6  is_exec_frag_def
    33.7 -  "is_exec_frag A ex ==  ((is_exec_fragC A`(snd ex)) (fst ex) ~= FF)"
    33.8 +  "is_exec_frag A ex ==  ((is_exec_fragC A$(snd ex)) (fst ex) ~= FF)"
    33.9  
   33.10  
   33.11  is_exec_fragC_def
   33.12 -  "is_exec_fragC A ==(fix`(LAM h ex. (%s. case ex of 
   33.13 +  "is_exec_fragC A ==(fix$(LAM h ex. (%s. case ex of 
   33.14        nil => TT
   33.15      | x##xs => (flift1 
   33.16 -            (%p. Def ((s,p):trans_of A) andalso (h`xs) (snd p)) 
   33.17 -             `x)
   33.18 +            (%p. Def ((s,p):trans_of A) andalso (h$xs) (snd p)) 
   33.19 +             $x)
   33.20     )))" 
   33.21  
   33.22  
   33.23 @@ -100,7 +100,7 @@
   33.24  
   33.25  has_schedule_def
   33.26    "has_schedule ioa sch ==                                               
   33.27 -     (? ex:executions ioa. sch = filter_act`(snd ex))"
   33.28 +     (? ex:executions ioa. sch = filter_act$(snd ex))"
   33.29  
   33.30  schedules_def
   33.31    "schedules ioa == {sch. has_schedule ioa sch}"
   33.32 @@ -110,7 +110,7 @@
   33.33  
   33.34  has_trace_def
   33.35    "has_trace ioa tr ==                                               
   33.36 -     (? sch:schedules ioa. tr = Filter (%a. a:ext(ioa))`sch)"
   33.37 +     (? sch:schedules ioa. tr = Filter (%a. a:ext(ioa))$sch)"
   33.38   
   33.39  traces_def
   33.40    "traces ioa == {tr. has_trace ioa tr}"
   33.41 @@ -118,18 +118,18 @@
   33.42  
   33.43  mk_trace_def
   33.44    "mk_trace ioa == LAM tr. 
   33.45 -     Filter (%a. a:ext(ioa))`(filter_act`tr)"
   33.46 +     Filter (%a. a:ext(ioa))$(filter_act$tr)"
   33.47  
   33.48  
   33.49  (*  ------------------- Fair Traces ------------------------------ *)
   33.50  
   33.51  laststate_def
   33.52 -  "laststate ex == case Last`(snd ex) of
   33.53 +  "laststate ex == case Last$(snd ex) of
   33.54                        Undef  => fst ex
   33.55                      | Def at => snd at"
   33.56  
   33.57  inf_often_def
   33.58 -  "inf_often P s == Infinite (Filter P`s)"
   33.59 +  "inf_often P s == Infinite (Filter P$s)"
   33.60  
   33.61  (*  filtering P yields a finite or partial sequence *)
   33.62  fin_often_def
   33.63 @@ -166,7 +166,7 @@
   33.64    "fairexecutions A == {ex. ex:executions A & fair_ex A ex}"
   33.65  
   33.66  fairtraces_def
   33.67 -  "fairtraces A == {mk_trace A`(snd ex) | ex. ex:fairexecutions A}"
   33.68 +  "fairtraces A == {mk_trace A$(snd ex) | ex. ex:fairexecutions A}"
   33.69  
   33.70  
   33.71  (*  ------------------- Implementation ------------------------------ *)
    34.1 --- a/src/HOLCF/domain/theorems.ML	Tue Jan 09 15:32:27 2001 +0100
    34.2 +++ b/src/HOLCF/domain/theorems.ML	Tue Jan 09 15:36:30 2001 +0100
    34.3 @@ -451,7 +451,7 @@
    34.4                                    asm_simp_tac take_ss 1 ::
    34.5                                    map (fn arg =>
    34.6                                     case_UU_tac (prems@con_rews) 1 (
    34.7 -                           nth_elem(rec_of arg,dnames)^"_take n`"^vname arg))
    34.8 +                           nth_elem(rec_of arg,dnames)^"_take n$"^vname arg))
    34.9                                    (filter is_nonlazy_rec args) @ [
   34.10                                    resolve_tac prems 1] @
   34.11                                    map (K (atac 1))      (nonlazy args) @
    35.1 --- a/src/HOLCF/ex/Dagstuhl.thy	Tue Jan 09 15:32:27 2001 +0100
    35.2 +++ b/src/HOLCF/ex/Dagstuhl.thy	Tue Jan 09 15:36:30 2001 +0100
    35.3 @@ -10,8 +10,8 @@
    35.4  
    35.5  defs
    35.6  
    35.7 -YS_def    "YS  == fix`(LAM x. y && x)"
    35.8 -YYS_def   "YYS == fix`(LAM z. y && y && z)"
    35.9 +YS_def    "YS  == fix$(LAM x. y && x)"
   35.10 +YYS_def   "YYS == fix$(LAM z. y && y && z)"
   35.11    
   35.12  end
   35.13  
    36.1 --- a/src/HOLCF/ex/Dnat.ML	Tue Jan 09 15:32:27 2001 +0100
    36.2 +++ b/src/HOLCF/ex/Dnat.ML	Tue Jan 09 15:36:30 2001 +0100
    36.3 @@ -13,23 +13,23 @@
    36.4  
    36.5  bind_thm ("iterator_def2", fix_prover2 Dnat.thy iterator_def 
    36.6  	"iterator = (LAM n f x. case n of dzero => x | \
    36.7 -\                                     dsucc`m => f`(iterator`m`f`x))");
    36.8 +\                                     dsucc$m => f$(iterator$m$f$x))");
    36.9  
   36.10  (* ------------------------------------------------------------------------- *)
   36.11  (* recursive  properties                                                     *)
   36.12  (* ------------------------------------------------------------------------- *)
   36.13  
   36.14 -Goal "iterator`UU`f`x = UU";
   36.15 +Goal "iterator$UU$f$x = UU";
   36.16  by (stac iterator_def2 1);
   36.17  by (simp_tac (HOLCF_ss addsimps dnat.rews) 1);
   36.18  qed "iterator1";
   36.19  
   36.20 -Goal "iterator`dzero`f`x = x";
   36.21 +Goal "iterator$dzero$f$x = x";
   36.22  by (stac iterator_def2 1);
   36.23  by (simp_tac (HOLCF_ss addsimps dnat.rews) 1);
   36.24  qed "iterator2";
   36.25  
   36.26 -Goal "n~=UU ==> iterator`(dsucc`n)`f`x = f`(iterator`n`f`x)";
   36.27 +Goal "n~=UU ==> iterator$(dsucc$n)$f$x = f$(iterator$n$f$x)";
   36.28  by (rtac trans 1);
   36.29  by (stac iterator_def2 1);
   36.30  by (asm_simp_tac (HOLCF_ss addsimps dnat.rews) 1);
    37.1 --- a/src/HOLCF/ex/Dnat.thy	Tue Jan 09 15:32:27 2001 +0100
    37.2 +++ b/src/HOLCF/ex/Dnat.thy	Tue Jan 09 15:36:30 2001 +0100
    37.3 @@ -13,7 +13,7 @@
    37.4  constdefs
    37.5  
    37.6  iterator :: "dnat -> ('a -> 'a) -> 'a -> 'a"
    37.7 -            "iterator == fix`(LAM h n f x . case n of dzero   => x
    37.8 -                                                    | dsucc`m => f`(h`m`f`x))"
    37.9 +            "iterator == fix$(LAM h n f x . case n of dzero   => x
   37.10 +                                                    | dsucc$m => f$(h$m$f$x))"
   37.11  
   37.12  end
    38.1 --- a/src/HOLCF/ex/Fix2.ML	Tue Jan 09 15:32:27 2001 +0100
    38.2 +++ b/src/HOLCF/ex/Fix2.ML	Tue Jan 09 15:36:30 2001 +0100
    38.3 @@ -14,7 +14,7 @@
    38.4  qed "lemma1";
    38.5  
    38.6  
    38.7 -Goal "gix`F=lub(range(%i. iterate i F UU))";
    38.8 +Goal "gix$F=lub(range(%i. iterate i F UU))";
    38.9  by (rtac (lemma1 RS subst) 1);
   38.10  by (rtac fix_def2 1);
   38.11  qed "lemma2";
    39.1 --- a/src/HOLCF/ex/Fix2.thy	Tue Jan 09 15:32:27 2001 +0100
    39.2 +++ b/src/HOLCF/ex/Fix2.thy	Tue Jan 09 15:36:30 2001 +0100
    39.3 @@ -16,7 +16,7 @@
    39.4  
    39.5  rules
    39.6  
    39.7 -gix1_def "F`(gix`F) = gix`F"
    39.8 -gix2_def "F`y=y ==> gix`F << y"
    39.9 +gix1_def "F$(gix$F) = gix$F"
   39.10 +gix2_def "F$y=y ==> gix$F << y"
   39.11  
   39.12  end
    40.1 --- a/src/HOLCF/ex/Focus_ex.ML	Tue Jan 09 15:32:27 2001 +0100
    40.2 +++ b/src/HOLCF/ex/Focus_ex.ML	Tue Jan 09 15:36:30 2001 +0100
    40.3 @@ -4,20 +4,20 @@
    40.4  
    40.5  val prems = goal Focus_ex.thy
    40.6  "is_g(g) = \ 
    40.7 -\ (? f. is_f(f) &  (!x.(? z. <g`x,z> = f`<x,z> &  \
    40.8 -\                  (! w y. <y,w> = f`<x,w>  --> z << w))))";
    40.9 +\ (? f. is_f(f) &  (!x.(? z. <g$x,z> = f$<x,z> &  \
   40.10 +\                  (! w y. <y,w> = f$<x,w>  --> z << w))))";
   40.11  by (simp_tac (HOL_ss addsimps [is_g,is_net_g]) 1);
   40.12  by (fast_tac HOL_cs 1);
   40.13  val lemma1 = result();
   40.14  
   40.15  val prems = goal Focus_ex.thy
   40.16 -"(? f. is_f(f) &  (!x. (? z. <g`x,z> = f`<x,z> &  \
   40.17 -\                 (!w y. <y,w> = f`<x,w>  --> z << w)))) \
   40.18 +"(? f. is_f(f) &  (!x. (? z. <g$x,z> = f$<x,z> &  \
   40.19 +\                 (!w y. <y,w> = f$<x,w>  --> z << w)))) \
   40.20  \ = \ 
   40.21  \ (? f. is_f(f) &  (!x. ? z.\
   40.22 -\       g`x = cfst`(f`<x,z>) &  \
   40.23 -\         z = csnd`(f`<x,z>) &  \
   40.24 -\       (! w y.  <y,w> = f`<x,w> --> z << w)))";
   40.25 +\       g$x = cfst$(f$<x,z>) &  \
   40.26 +\         z = csnd$(f$<x,z>) &  \
   40.27 +\       (! w y.  <y,w> = f$<x,w> --> z << w)))";
   40.28  by (rtac iffI 1);
   40.29  by (etac exE 1);
   40.30  by (res_inst_tac [("x","f")] exI 1);
   40.31 @@ -63,7 +63,7 @@
   40.32  by (REPEAT (etac conjE 1));
   40.33  by (etac conjI 1);
   40.34  by (strip_tac 1);
   40.35 -by (res_inst_tac [("x","fix`(LAM k. csnd`(f`<x,k>))")] exI 1);
   40.36 +by (res_inst_tac [("x","fix$(LAM k. csnd$(f$<x,k>))")] exI 1);
   40.37  by (rtac conjI 1);
   40.38   by (asm_simp_tac HOLCF_ss 1);
   40.39   by (rtac trans 1);
   40.40 @@ -94,16 +94,16 @@
   40.41  by (eres_inst_tac [("x","x")] allE 1);
   40.42  by (etac exE 1);
   40.43  by (REPEAT (etac conjE 1));
   40.44 -by (subgoal_tac "fix`(LAM k. csnd`(f`<x, k>)) = z" 1);
   40.45 +by (subgoal_tac "fix$(LAM k. csnd$(f$<x, k>)) = z" 1);
   40.46   by (asm_simp_tac HOLCF_ss 1);
   40.47 -by (subgoal_tac "! w y. f`<x, w> = <y, w>  --> z << w" 1);
   40.48 +by (subgoal_tac "! w y. f$<x, w> = <y, w>  --> z << w" 1);
   40.49  by (rtac sym 1);
   40.50  by (rtac fix_eqI 1);
   40.51  by (asm_simp_tac HOLCF_ss 1);
   40.52  by (rtac allI 1);
   40.53  by (simp_tac HOLCF_ss 1);
   40.54  by (strip_tac 1);
   40.55 -by (subgoal_tac "f`<x, za> = <cfst`(f`<x,za>),za>" 1);
   40.56 +by (subgoal_tac "f$<x, za> = <cfst$(f$<x,za>),za>" 1);
   40.57  by (fast_tac HOL_cs 1);
   40.58  by (rtac trans 1);
   40.59  by (rtac (surjective_pairing_Cprod2 RS sym) 1);
    41.1 --- a/src/HOLCF/ex/Focus_ex.thy	Tue Jan 09 15:32:27 2001 +0100
    41.2 +++ b/src/HOLCF/ex/Focus_ex.thy	Tue Jan 09 15:36:30 2001 +0100
    41.3 @@ -30,7 +30,7 @@
    41.4  	input  channel x:'b 
    41.5  	output channel y:'c 
    41.6  is network
    41.7 -	<y,z> = f`<x,z>
    41.8 +	<y,z> = f$<x,z>
    41.9  end network
   41.10  end g
   41.11  
   41.12 @@ -47,7 +47,7 @@
   41.13  		'c stream * ('b,'c) tc stream) => bool
   41.14  
   41.15  is_f f  = !i1 i2 o1 o2. 
   41.16 -	f`<i1,i2> = <o1,o2> --> Rf(i1,i2,o1,o2)
   41.17 +	f$<i1,i2> = <o1,o2> --> Rf(i1,i2,o1,o2)
   41.18  
   41.19  Specification of agent g is translated to predicate is_g which uses
   41.20  predicate is_net_g
   41.21 @@ -56,13 +56,13 @@
   41.22  	    'b stream => 'c stream => bool
   41.23  
   41.24  is_net_g f x y = 
   41.25 -	? z. <y,z> = f`<x,z> & 
   41.26 -	!oy hz. <oy,hz> = f`<x,hz> --> z << hz 
   41.27 +	? z. <y,z> = f$<x,z> & 
   41.28 +	!oy hz. <oy,hz> = f$<x,hz> --> z << hz 
   41.29  
   41.30  
   41.31  is_g :: ('b stream -> 'c stream) => bool
   41.32  
   41.33 -is_g g  = ? f. is_f f  & (!x y. g`x = y --> is_net_g f x y
   41.34 +is_g g  = ? f. is_f f  & (!x y. g$x = y --> is_net_g f x y
   41.35  	  
   41.36  Third step: (show conservativity)
   41.37  -----------
   41.38 @@ -84,7 +84,7 @@
   41.39  
   41.40  def_g g  = 
   41.41           (? f. is_f f  & 
   41.42 -	      g = (LAM x. cfst`(f`<x,fix`(LAM k.csnd`(f`<x,k>))>)) )
   41.43 +	      g = (LAM x. cfst$(f$<x,fix$(LAM k.csnd$(f$<x,k>))>)) )
   41.44  	
   41.45  Now we prove:
   41.46  
   41.47 @@ -118,19 +118,19 @@
   41.48  defs
   41.49  
   41.50  is_f		"is_f f == (!i1 i2 o1 o2.
   41.51 -			f`<i1,i2> = <o1,o2> --> Rf(i1,i2,o1,o2))"
   41.52 +			f$<i1,i2> = <o1,o2> --> Rf(i1,i2,o1,o2))"
   41.53  
   41.54  is_net_g	"is_net_g f x y == (? z. 
   41.55 -			<y,z> = f`<x,z> &
   41.56 -			(!oy hz. <oy,hz> = f`<x,hz> --> z << hz))" 
   41.57 +			<y,z> = f$<x,z> &
   41.58 +			(!oy hz. <oy,hz> = f$<x,hz> --> z << hz))" 
   41.59  
   41.60  is_g		"is_g g  == (? f.
   41.61  			is_f f  & 
   41.62 -			(!x y. g`x = y --> is_net_g f x y))"
   41.63 +			(!x y. g$x = y --> is_net_g f x y))"
   41.64  
   41.65  
   41.66  def_g		"def_g g == (? f.
   41.67  			is_f f  & 
   41.68 -	      		g = (LAM x. cfst`(f`<x,fix`(LAM  k. csnd`(f`<x,k>))>)))" 
   41.69 +	      		g = (LAM x. cfst$(f$<x,fix$(LAM  k. csnd$(f$<x,k>))>)))" 
   41.70  
   41.71  end
    42.1 --- a/src/HOLCF/ex/Hoare.ML	Tue Jan 09 15:32:27 2001 +0100
    42.2 +++ b/src/HOLCF/ex/Hoare.ML	Tue Jan 09 15:36:30 2001 +0100
    42.3 @@ -14,21 +14,21 @@
    42.4  by (fast_tac HOL_cs 1);
    42.5  qed "hoare_lemma2";
    42.6  
    42.7 -Goal " (ALL k. b1`(iterate k g x) = TT) | (EX k. b1`(iterate k g x)~=TT)";
    42.8 +Goal " (ALL k. b1$(iterate k g x) = TT) | (EX k. b1$(iterate k g x)~=TT)";
    42.9  by (fast_tac HOL_cs 1);
   42.10  qed "hoare_lemma3";
   42.11  
   42.12 -Goal "(EX k. b1`(iterate k g x) ~= TT) ==> \
   42.13 -\ EX k. b1`(iterate k g x) = FF | b1`(iterate k g x) = UU";
   42.14 +Goal "(EX k. b1$(iterate k g x) ~= TT) ==> \
   42.15 +\ EX k. b1$(iterate k g x) = FF | b1$(iterate k g x) = UU";
   42.16  by (etac exE 1);
   42.17  by (rtac exI 1);
   42.18  by (rtac hoare_lemma2 1);
   42.19  by (atac 1);
   42.20  qed "hoare_lemma4";
   42.21  
   42.22 -Goal "[|(EX k. b1`(iterate k g x) ~= TT);\
   42.23 -\   k=Least(%n. b1`(iterate n g x) ~= TT)|] ==> \
   42.24 -\ b1`(iterate k g x)=FF | b1`(iterate k g x)=UU";
   42.25 +Goal "[|(EX k. b1$(iterate k g x) ~= TT);\
   42.26 +\   k=Least(%n. b1$(iterate n g x) ~= TT)|] ==> \
   42.27 +\ b1$(iterate k g x)=FF | b1$(iterate k g x)=UU";
   42.28  by (hyp_subst_tac 1);
   42.29  by (rtac hoare_lemma2 1);
   42.30  by (etac exE 1);
   42.31 @@ -45,13 +45,13 @@
   42.32  by (resolve_tac dist_eq_tr 1);
   42.33  qed "hoare_lemma7";
   42.34  
   42.35 -Goal "[|(EX k. b1`(iterate k g x) ~= TT);\
   42.36 -\   k=Least(%n. b1`(iterate n g x) ~= TT)|] ==> \
   42.37 -\ ALL m. m < k --> b1`(iterate m g x)=TT";
   42.38 +Goal "[|(EX k. b1$(iterate k g x) ~= TT);\
   42.39 +\   k=Least(%n. b1$(iterate n g x) ~= TT)|] ==> \
   42.40 +\ ALL m. m < k --> b1$(iterate m g x)=TT";
   42.41  by (hyp_subst_tac 1);
   42.42  by (etac exE 1);
   42.43  by (strip_tac 1);
   42.44 -by (res_inst_tac [("p","b1`(iterate m g x)")] trE 1);
   42.45 +by (res_inst_tac [("p","b1$(iterate m g x)")] trE 1);
   42.46  by (atac 2);
   42.47  by (rtac (le_less_trans RS less_irrefl) 1);
   42.48  by (atac 2);
   42.49 @@ -64,7 +64,7 @@
   42.50  qed "hoare_lemma8";
   42.51  
   42.52  
   42.53 -Goal "f`(y::'a)=(UU::tr) ==> f`UU = UU";
   42.54 +Goal "f$(y::'a)=(UU::tr) ==> f$UU = UU";
   42.55  by (etac (flat_codom RS disjE) 1);
   42.56  by Auto_tac;  
   42.57  qed "hoare_lemma28";
   42.58 @@ -72,28 +72,28 @@
   42.59  
   42.60  (* ----- access to definitions ----- *)
   42.61  
   42.62 -Goal "p`x = If b1`x then p`(g`x) else x fi";
   42.63 +Goal "p$x = If b1$x then p$(g$x) else x fi";
   42.64  by (fix_tac3 p_def 1);
   42.65  by (Simp_tac 1);
   42.66  qed "p_def3";
   42.67  
   42.68 -Goal "q`x = If b1`x orelse b2`x then q`(g`x) else x fi";
   42.69 +Goal "q$x = If b1$x orelse b2$x then q$(g$x) else x fi";
   42.70  by (fix_tac3 q_def 1);
   42.71  by (Simp_tac 1);
   42.72  qed "q_def3";
   42.73  
   42.74  (** --------- proves about iterations of p and q ---------- **)
   42.75  
   42.76 -Goal "(ALL m. m< Suc k --> b1`(iterate m g x)=TT) -->\
   42.77 -\  p`(iterate k g x)=p`x";
   42.78 +Goal "(ALL m. m< Suc k --> b1$(iterate m g x)=TT) -->\
   42.79 +\  p$(iterate k g x)=p$x";
   42.80  by (nat_ind_tac "k" 1);
   42.81  by (Simp_tac 1);
   42.82  by (Simp_tac 1);
   42.83  by (strip_tac 1);
   42.84 -by (res_inst_tac [("s","p`(iterate k g x)")] trans 1);
   42.85 +by (res_inst_tac [("s","p$(iterate k g x)")] trans 1);
   42.86  by (rtac trans 1);
   42.87  by (rtac (p_def3 RS sym) 2);
   42.88 -by (res_inst_tac [("s","TT"),("t","b1`(iterate k g x)")] ssubst 1);
   42.89 +by (res_inst_tac [("s","TT"),("t","b1$(iterate k g x)")] ssubst 1);
   42.90  by (rtac mp 1);
   42.91  by (etac spec 1);
   42.92  by (simp_tac (simpset() addsimps [less_Suc_eq]) 1);
   42.93 @@ -106,16 +106,16 @@
   42.94  by (Simp_tac 1);
   42.95  qed "hoare_lemma9";
   42.96  
   42.97 -Goal "(ALL m. m< Suc k --> b1`(iterate m g x)=TT) --> \
   42.98 -\ q`(iterate k g x)=q`x";
   42.99 +Goal "(ALL m. m< Suc k --> b1$(iterate m g x)=TT) --> \
  42.100 +\ q$(iterate k g x)=q$x";
  42.101  by (nat_ind_tac "k" 1);
  42.102  by (Simp_tac 1);
  42.103  by (simp_tac (simpset() addsimps [less_Suc_eq]) 1);
  42.104  by (strip_tac 1);
  42.105 -by (res_inst_tac [("s","q`(iterate k g x)")] trans 1);
  42.106 +by (res_inst_tac [("s","q$(iterate k g x)")] trans 1);
  42.107  by (rtac trans 1);
  42.108  by (rtac (q_def3 RS sym) 2);
  42.109 -by (res_inst_tac [("s","TT"),("t","b1`(iterate k g x)")] ssubst 1);
  42.110 +by (res_inst_tac [("s","TT"),("t","b1$(iterate k g x)")] ssubst 1);
  42.111  by (fast_tac HOL_cs 1);
  42.112  by (simp_tac HOLCF_ss 1);
  42.113  by (etac mp 1);
  42.114 @@ -123,20 +123,20 @@
  42.115  by (fast_tac (HOL_cs addSDs [less_Suc_eq RS iffD1]) 1);
  42.116  qed "hoare_lemma24";
  42.117  
  42.118 -(* -------- results about p for case (EX k. b1`(iterate k g x)~=TT) ------- *)
  42.119 +(* -------- results about p for case (EX k. b1$(iterate k g x)~=TT) ------- *)
  42.120  
  42.121  
  42.122  val hoare_lemma10 = (hoare_lemma8 RS (hoare_lemma9 RS mp));
  42.123  (* 
  42.124 -val hoare_lemma10 = "[| EX k. b1`(iterate k g ?x1) ~= TT;
  42.125 -    Suc ?k3 = Least(%n. b1`(iterate n g ?x1) ~= TT) |] ==>
  42.126 - p`(iterate ?k3 g ?x1) = p`?x1" : thm
  42.127 +val hoare_lemma10 = "[| EX k. b1$(iterate k g ?x1) ~= TT;
  42.128 +    Suc ?k3 = Least(%n. b1$(iterate n g ?x1) ~= TT) |] ==>
  42.129 + p$(iterate ?k3 g ?x1) = p$?x1" : thm
  42.130  
  42.131  *)
  42.132  
  42.133 -Goal "(EX n. b1`(iterate n g x) ~= TT) ==>\
  42.134 -\ k=(LEAST n. b1`(iterate n g x) ~= TT) & b1`(iterate k g x)=FF \
  42.135 -\ --> p`x = iterate k g x";
  42.136 +Goal "(EX n. b1$(iterate n g x) ~= TT) ==>\
  42.137 +\ k=(LEAST n. b1$(iterate n g x) ~= TT) & b1$(iterate k g x)=FF \
  42.138 +\ --> p$x = iterate k g x";
  42.139  by (case_tac "k" 1);
  42.140  by (hyp_subst_tac 1);
  42.141  by (Simp_tac 1);
  42.142 @@ -153,7 +153,7 @@
  42.143  by (atac 1);
  42.144  by (rtac trans 1);
  42.145  by (rtac p_def3 1);
  42.146 -by (res_inst_tac [("s","TT"),("t","b1`(iterate nat g x)")] ssubst 1);
  42.147 +by (res_inst_tac [("s","TT"),("t","b1$(iterate nat g x)")] ssubst 1);
  42.148  by (rtac (hoare_lemma8 RS spec RS mp) 1);
  42.149  by (atac 1);
  42.150  by (atac 1);
  42.151 @@ -166,9 +166,9 @@
  42.152  by (simp_tac HOLCF_ss 1);
  42.153  qed "hoare_lemma11";
  42.154  
  42.155 -Goal "(EX n. b1`(iterate n g x) ~= TT) ==>\
  42.156 -\ k=Least(%n. b1`(iterate n g x)~=TT) & b1`(iterate k g x)=UU \
  42.157 -\ --> p`x = UU";
  42.158 +Goal "(EX n. b1$(iterate n g x) ~= TT) ==>\
  42.159 +\ k=Least(%n. b1$(iterate n g x)~=TT) & b1$(iterate k g x)=UU \
  42.160 +\ --> p$x = UU";
  42.161  by (case_tac "k" 1);
  42.162  by (hyp_subst_tac 1);
  42.163  by (Simp_tac 1);
  42.164 @@ -187,7 +187,7 @@
  42.165  by (atac 1);
  42.166  by (rtac trans 1);
  42.167  by (rtac p_def3 1);
  42.168 -by (res_inst_tac [("s","TT"),("t","b1`(iterate nat g x)")] ssubst 1);
  42.169 +by (res_inst_tac [("s","TT"),("t","b1$(iterate nat g x)")] ssubst 1);
  42.170  by (rtac (hoare_lemma8 RS spec RS mp) 1);
  42.171  by (atac 1);
  42.172  by (atac 1);
  42.173 @@ -198,9 +198,9 @@
  42.174  by (asm_simp_tac HOLCF_ss 1);
  42.175  qed "hoare_lemma12";
  42.176  
  42.177 -(* -------- results about p for case  (ALL k. b1`(iterate k g x)=TT) ------- *)
  42.178 +(* -------- results about p for case  (ALL k. b1$(iterate k g x)=TT) ------- *)
  42.179  
  42.180 -Goal "(ALL k. b1`(iterate k g x)=TT) ==> ALL k. p`(iterate k g x) = UU";
  42.181 +Goal "(ALL k. b1$(iterate k g x)=TT) ==> ALL k. p$(iterate k g x) = UU";
  42.182  by (rtac (p_def RS def_fix_ind) 1);
  42.183  by (rtac adm_all 1);
  42.184  by (rtac allI 1);
  42.185 @@ -211,21 +211,21 @@
  42.186  by (rtac refl 1);
  42.187  by (Simp_tac 1);
  42.188  by (rtac allI 1);
  42.189 -by (res_inst_tac [("s","TT"),("t","b1`(iterate k g x)")] ssubst 1);
  42.190 +by (res_inst_tac [("s","TT"),("t","b1$(iterate k g x)")] ssubst 1);
  42.191  by (etac spec 1);
  42.192  by (asm_simp_tac HOLCF_ss 1);
  42.193  by (rtac (iterate_Suc RS subst) 1);
  42.194  by (etac spec 1);
  42.195  qed "fernpass_lemma";
  42.196  
  42.197 -Goal "(ALL k. b1`(iterate k g x)=TT) ==> p`x = UU";
  42.198 +Goal "(ALL k. b1$(iterate k g x)=TT) ==> p$x = UU";
  42.199  by (res_inst_tac [("F1","g"),("t","x")] (iterate_0 RS subst) 1);
  42.200  by (etac (fernpass_lemma RS spec) 1);
  42.201  qed "hoare_lemma16";
  42.202  
  42.203 -(* -------- results about q for case  (ALL k. b1`(iterate k g x)=TT) ------- *)
  42.204 +(* -------- results about q for case  (ALL k. b1$(iterate k g x)=TT) ------- *)
  42.205  
  42.206 -Goal "(ALL k. b1`(iterate k g x)=TT) ==> ALL k. q`(iterate k g x) = UU";
  42.207 +Goal "(ALL k. b1$(iterate k g x)=TT) ==> ALL k. q$(iterate k g x) = UU";
  42.208  by (rtac (q_def RS def_fix_ind) 1);
  42.209  by (rtac adm_all 1);
  42.210  by (rtac allI 1);
  42.211 @@ -236,25 +236,25 @@
  42.212  by (rtac refl 1);
  42.213  by (rtac allI 1);
  42.214  by (Simp_tac 1);
  42.215 -by (res_inst_tac [("s","TT"),("t","b1`(iterate k g x)")] ssubst 1);
  42.216 +by (res_inst_tac [("s","TT"),("t","b1$(iterate k g x)")] ssubst 1);
  42.217  by (etac spec 1);
  42.218  by (asm_simp_tac HOLCF_ss 1);
  42.219  by (rtac (iterate_Suc RS subst) 1);
  42.220  by (etac spec 1);
  42.221  qed "hoare_lemma17";
  42.222  
  42.223 -Goal "(ALL k. b1`(iterate k g x)=TT) ==> q`x = UU";
  42.224 +Goal "(ALL k. b1$(iterate k g x)=TT) ==> q$x = UU";
  42.225  by (res_inst_tac [("F1","g"),("t","x")] (iterate_0 RS subst) 1);
  42.226  by (etac (hoare_lemma17 RS spec) 1);
  42.227  qed "hoare_lemma18";
  42.228  
  42.229 -Goal "(ALL k. (b1::'a->tr)`(iterate k g x)=TT) ==> b1`(UU::'a) = UU | (ALL y. b1`(y::'a)=TT)";
  42.230 +Goal "(ALL k. (b1::'a->tr)$(iterate k g x)=TT) ==> b1$(UU::'a) = UU | (ALL y. b1$(y::'a)=TT)";
  42.231  by (rtac (flat_codom) 1);
  42.232  by (res_inst_tac [("t","x1")] (iterate_0 RS subst) 1);
  42.233  by (etac spec 1);
  42.234  qed "hoare_lemma19";
  42.235  
  42.236 -Goal "(ALL y. b1`(y::'a)=TT) ==> ALL k. q`(iterate k g (x::'a)) = UU";
  42.237 +Goal "(ALL y. b1$(y::'a)=TT) ==> ALL k. q$(iterate k g (x::'a)) = UU";
  42.238  by (rtac (q_def RS def_fix_ind) 1);
  42.239  by (rtac adm_all 1);
  42.240  by (rtac allI 1);
  42.241 @@ -265,35 +265,35 @@
  42.242  by (rtac refl 1);
  42.243  by (rtac allI 1);
  42.244  by (Simp_tac 1);
  42.245 -by (res_inst_tac [("s","TT"),("t","b1`(iterate k g (x::'a))")] ssubst 1);
  42.246 +by (res_inst_tac [("s","TT"),("t","b1$(iterate k g (x::'a))")] ssubst 1);
  42.247  by (etac spec 1);
  42.248  by (asm_simp_tac HOLCF_ss 1);
  42.249  by (rtac (iterate_Suc RS subst) 1);
  42.250  by (etac spec 1);
  42.251  qed "hoare_lemma20";
  42.252  
  42.253 -Goal "(ALL y. b1`(y::'a)=TT) ==> q`(x::'a) = UU";
  42.254 +Goal "(ALL y. b1$(y::'a)=TT) ==> q$(x::'a) = UU";
  42.255  by (res_inst_tac [("F1","g"),("t","x")] (iterate_0 RS subst) 1);
  42.256  by (etac (hoare_lemma20 RS spec) 1);
  42.257  qed "hoare_lemma21";
  42.258  
  42.259 -Goal "b1`(UU::'a)=UU ==> q`(UU::'a) = UU";
  42.260 +Goal "b1$(UU::'a)=UU ==> q$(UU::'a) = UU";
  42.261  by (stac q_def3 1);
  42.262  by (asm_simp_tac HOLCF_ss 1);
  42.263  qed "hoare_lemma22";
  42.264  
  42.265 -(* -------- results about q for case (EX k. b1`(iterate k g x) ~= TT) ------- *)
  42.266 +(* -------- results about q for case (EX k. b1$(iterate k g x) ~= TT) ------- *)
  42.267  
  42.268  val hoare_lemma25 = (hoare_lemma8 RS (hoare_lemma24 RS mp) );
  42.269  (* 
  42.270 -val hoare_lemma25 = "[| EX k. b1`(iterate k g ?x1) ~= TT;
  42.271 -    Suc ?k3 = Least(%n. b1`(iterate n g ?x1) ~= TT) |] ==>
  42.272 - q`(iterate ?k3 g ?x1) = q`?x1" : thm
  42.273 +val hoare_lemma25 = "[| EX k. b1$(iterate k g ?x1) ~= TT;
  42.274 +    Suc ?k3 = Least(%n. b1$(iterate n g ?x1) ~= TT) |] ==>
  42.275 + q$(iterate ?k3 g ?x1) = q$?x1" : thm
  42.276  *)
  42.277  
  42.278 -Goal "(EX n. b1`(iterate n g x)~=TT) ==>\
  42.279 -\ k=Least(%n. b1`(iterate n g x) ~= TT) & b1`(iterate k g x) =FF \
  42.280 -\ --> q`x = q`(iterate k g x)";
  42.281 +Goal "(EX n. b1$(iterate n g x)~=TT) ==>\
  42.282 +\ k=Least(%n. b1$(iterate n g x) ~= TT) & b1$(iterate k g x) =FF \
  42.283 +\ --> q$x = q$(iterate k g x)";
  42.284  by (case_tac "k" 1);
  42.285  by (hyp_subst_tac 1);
  42.286  by (strip_tac 1);
  42.287 @@ -307,7 +307,7 @@
  42.288  by (atac 1);
  42.289  by (rtac trans 1);
  42.290  by (rtac q_def3 1);
  42.291 -by (res_inst_tac [("s","TT"),("t","b1`(iterate nat g x)")] ssubst 1);
  42.292 +by (res_inst_tac [("s","TT"),("t","b1$(iterate nat g x)")] ssubst 1);
  42.293  by (rtac (hoare_lemma8 RS spec RS mp) 1);
  42.294  by (atac 1);
  42.295  by (atac 1);
  42.296 @@ -316,9 +316,9 @@
  42.297  qed "hoare_lemma26";
  42.298  
  42.299  
  42.300 -Goal "(EX n. b1`(iterate n g x) ~= TT) ==>\
  42.301 -\ k=Least(%n. b1`(iterate n g x)~=TT) & b1`(iterate k g x)=UU \
  42.302 -\ --> q`x = UU";
  42.303 +Goal "(EX n. b1$(iterate n g x) ~= TT) ==>\
  42.304 +\ k=Least(%n. b1$(iterate n g x)~=TT) & b1$(iterate k g x)=UU \
  42.305 +\ --> q$x = UU";
  42.306  by (case_tac "k" 1);
  42.307  by (hyp_subst_tac 1);
  42.308  by (Simp_tac 1);
  42.309 @@ -336,7 +336,7 @@
  42.310  by (atac 1);
  42.311  by (rtac trans 1);
  42.312  by (rtac q_def3 1);
  42.313 -by (res_inst_tac [("s","TT"),("t","b1`(iterate nat g x)")] ssubst 1);
  42.314 +by (res_inst_tac [("s","TT"),("t","b1$(iterate nat g x)")] ssubst 1);
  42.315  by (rtac (hoare_lemma8 RS spec RS mp) 1);
  42.316  by (atac 1);
  42.317  by (atac 1);
  42.318 @@ -347,9 +347,9 @@
  42.319  by (asm_simp_tac HOLCF_ss 1);
  42.320  qed "hoare_lemma27";
  42.321  
  42.322 -(* ------- (ALL k. b1`(iterate k g x)=TT) ==> q o p = q   ----- *)
  42.323 +(* ------- (ALL k. b1$(iterate k g x)=TT) ==> q o p = q   ----- *)
  42.324  
  42.325 -Goal "(ALL k. b1`(iterate k g x)=TT) ==> q`(p`x) = q`x";
  42.326 +Goal "(ALL k. b1$(iterate k g x)=TT) ==> q$(p$x) = q$x";
  42.327  by (stac hoare_lemma16 1);
  42.328  by (atac 1);
  42.329  by (rtac (hoare_lemma19 RS disjE) 1);
  42.330 @@ -368,7 +368,7 @@
  42.331  
  42.332  (* ------------  EX k. b1~(iterate k g x) ~= TT ==> q o p = q   ----- *)
  42.333  
  42.334 -Goal "EX k. b1`(iterate k g x) ~= TT ==> q`(p`x) = q`x";
  42.335 +Goal "EX k. b1$(iterate k g x) ~= TT ==> q$(p$x) = q$x";
  42.336  by (rtac (hoare_lemma5 RS disjE) 1);
  42.337  by (atac 1);
  42.338  by (rtac refl 1);
    43.1 --- a/src/HOLCF/ex/Hoare.thy	Tue Jan 09 15:32:27 2001 +0100
    43.2 +++ b/src/HOLCF/ex/Hoare.thy	Tue Jan 09 15:36:30 2001 +0100
    43.3 @@ -32,11 +32,11 @@
    43.4  
    43.5  defs
    43.6  
    43.7 -  p_def  "p == fix`(LAM f. LAM x.
    43.8 -                 If b1`x then f`(g`x) else x fi)"
    43.9 +  p_def  "p == fix$(LAM f. LAM x.
   43.10 +                 If b1$x then f$(g$x) else x fi)"
   43.11  
   43.12 -  q_def  "q == fix`(LAM f. LAM x.
   43.13 -                 If b1`x orelse b2`x then f`(g`x) else x fi)"
   43.14 +  q_def  "q == fix$(LAM f. LAM x.
   43.15 +                 If b1$x orelse b2$x then f$(g$x) else x fi)"
   43.16  
   43.17  end
   43.18   
    44.1 --- a/src/HOLCF/ex/Loop.ML	Tue Jan 09 15:32:27 2001 +0100
    44.2 +++ b/src/HOLCF/ex/Loop.ML	Tue Jan 09 15:36:30 2001 +0100
    44.3 @@ -11,11 +11,11 @@
    44.4  (* ------------------------------------------------------------------------- *)
    44.5  
    44.6  
    44.7 -Goalw [step_def] "step`b`g`x = If b`x then g`x else x fi";
    44.8 +Goalw [step_def] "step$b$g$x = If b$x then g$x else x fi";
    44.9  by (Simp_tac 1);
   44.10  qed "step_def2";
   44.11  
   44.12 -Goalw [while_def] "while`b`g = fix`(LAM f x. If b`x then f`(g`x) else x fi)";
   44.13 +Goalw [while_def] "while$b$g = fix$(LAM f x. If b$x then f$(g$x) else x fi)";
   44.14  by (Simp_tac 1);
   44.15  qed "while_def2";
   44.16  
   44.17 @@ -24,12 +24,12 @@
   44.18  (* rekursive properties of while                                             *)
   44.19  (* ------------------------------------------------------------------------- *)
   44.20  
   44.21 -Goal "while`b`g`x = If b`x then while`b`g`(g`x) else x fi";
   44.22 +Goal "while$b$g$x = If b$x then while$b$g$(g$x) else x fi";
   44.23  by (fix_tac5  while_def2 1);
   44.24  by (Simp_tac 1);
   44.25  qed "while_unfold";
   44.26  
   44.27 -Goal "ALL x. while`b`g`x = while`b`g`(iterate k (step`b`g) x)";
   44.28 +Goal "ALL x. while$b$g$x = while$b$g$(iterate k (step$b$g) x)";
   44.29  by (nat_ind_tac "k" 1);
   44.30  by (simp_tac HOLCF_ss 1);
   44.31  by (rtac allI 1);
   44.32 @@ -40,10 +40,10 @@
   44.33  by (rtac trans 1);
   44.34  by (etac spec 2);
   44.35  by (stac step_def2 1);
   44.36 -by (res_inst_tac [("p","b`x")] trE 1);
   44.37 +by (res_inst_tac [("p","b$x")] trE 1);
   44.38  by (asm_simp_tac HOLCF_ss 1);
   44.39  by (stac while_unfold 1);
   44.40 -by (res_inst_tac [("s","UU"),("t","b`UU")]ssubst 1);
   44.41 +by (res_inst_tac [("s","UU"),("t","b$UU")]ssubst 1);
   44.42  by (etac (flat_codom RS disjE) 1);
   44.43  by (atac 1);
   44.44  by (etac spec 1);
   44.45 @@ -54,8 +54,8 @@
   44.46  by (asm_simp_tac HOLCF_ss 1);
   44.47  qed "while_unfold2";
   44.48  
   44.49 -Goal "while`b`g`x = while`b`g`(step`b`g`x)";
   44.50 -by (res_inst_tac [("s", "while`b`g`(iterate (Suc 0) (step`b`g) x)")] trans 1);
   44.51 +Goal "while$b$g$x = while$b$g$(step$b$g$x)";
   44.52 +by (res_inst_tac [("s", "while$b$g$(iterate (Suc 0) (step$b$g) x)")] trans 1);
   44.53  by (rtac (while_unfold2 RS spec) 1);
   44.54  by (Simp_tac 1);
   44.55  qed "while_unfold3";
   44.56 @@ -65,8 +65,8 @@
   44.57  (* properties of while and iterations                                        *)
   44.58  (* ------------------------------------------------------------------------- *)
   44.59  
   44.60 -Goal "[| EX y. b`y=FF; iterate k (step`b`g) x = UU |] \
   44.61 -\    ==>iterate(Suc k) (step`b`g) x=UU";
   44.62 +Goal "[| EX y. b$y=FF; iterate k (step$b$g) x = UU |] \
   44.63 +\    ==>iterate(Suc k) (step$b$g) x=UU";
   44.64  by (Simp_tac 1);
   44.65  by (rtac trans 1);
   44.66  by (rtac step_def2 1);
   44.67 @@ -77,34 +77,34 @@
   44.68  by (asm_simp_tac HOLCF_ss 1);
   44.69  qed "loop_lemma1";
   44.70  
   44.71 -Goal "[|EX y. b`y=FF;iterate (Suc k) (step`b`g) x ~=UU |]==>\
   44.72 -\     iterate k (step`b`g) x ~=UU";
   44.73 +Goal "[|EX y. b$y=FF;iterate (Suc k) (step$b$g) x ~=UU |]==>\
   44.74 +\     iterate k (step$b$g) x ~=UU";
   44.75  
   44.76  by (blast_tac (claset() addIs [loop_lemma1]) 1);
   44.77  qed "loop_lemma2";
   44.78  
   44.79 -Goal "[| ALL x. INV x & b`x=TT & g`x~=UU --> INV (g`x);\
   44.80 -\        EX y. b`y=FF; INV x |] \
   44.81 -\     ==> iterate k (step`b`g) x ~=UU --> INV (iterate k (step`b`g) x)";
   44.82 +Goal "[| ALL x. INV x & b$x=TT & g$x~=UU --> INV (g$x);\
   44.83 +\        EX y. b$y=FF; INV x |] \
   44.84 +\     ==> iterate k (step$b$g) x ~=UU --> INV (iterate k (step$b$g) x)";
   44.85  by (nat_ind_tac "k" 1);
   44.86  by (Asm_simp_tac 1);
   44.87  by (strip_tac 1);
   44.88  by (simp_tac (simpset() addsimps [step_def2]) 1);
   44.89 -by (res_inst_tac [("p","b`(iterate k (step`b`g) x)")] trE 1);
   44.90 +by (res_inst_tac [("p","b$(iterate k (step$b$g) x)")] trE 1);
   44.91  by (etac notE 1);
   44.92  by (asm_simp_tac (HOLCF_ss addsimps [step_def2] ) 1);
   44.93  by (asm_simp_tac HOLCF_ss 1);
   44.94  by (rtac mp 1);
   44.95  by (etac spec 1);
   44.96  by (asm_simp_tac (HOLCF_ss delsimps [iterate_Suc] addsimps [loop_lemma2] ) 1);
   44.97 -by (res_inst_tac [("s","iterate (Suc k) (step`b`g) x"),
   44.98 -                  ("t","g`(iterate k (step`b`g) x)")] ssubst 1);
   44.99 +by (res_inst_tac [("s","iterate (Suc k) (step$b$g) x"),
  44.100 +                  ("t","g$(iterate k (step$b$g) x)")] ssubst 1);
  44.101  by (atac 2);
  44.102  by (asm_simp_tac (HOLCF_ss addsimps [step_def2] ) 1);
  44.103  by (asm_simp_tac (HOLCF_ss delsimps [iterate_Suc] addsimps [loop_lemma2] ) 1);
  44.104  qed_spec_mp "loop_lemma3";
  44.105  
  44.106 -Goal "ALL x. b`(iterate k (step`b`g) x)=FF --> while`b`g`x= iterate k (step`b`g) x";
  44.107 +Goal "ALL x. b$(iterate k (step$b$g) x)=FF --> while$b$g$x= iterate k (step$b$g) x";
  44.108  by (nat_ind_tac "k" 1);
  44.109  by (Simp_tac 1);
  44.110  by (strip_tac 1);
  44.111 @@ -118,8 +118,8 @@
  44.112  by (Asm_simp_tac 1);
  44.113  qed_spec_mp "loop_lemma4";
  44.114  
  44.115 -Goal "ALL k. b`(iterate k (step`b`g) x) ~= FF ==>\
  44.116 -\ ALL m. while`b`g`(iterate m (step`b`g) x)=UU";
  44.117 +Goal "ALL k. b$(iterate k (step$b$g) x) ~= FF ==>\
  44.118 +\ ALL m. while$b$g$(iterate m (step$b$g) x)=UU";
  44.119  by (stac while_def2 1);
  44.120  by (rtac fix_ind 1);
  44.121  by (rtac (allI RS adm_all) 1);
  44.122 @@ -128,10 +128,10 @@
  44.123  by (Simp_tac  1);
  44.124  by (rtac allI 1);
  44.125  by (Simp_tac  1);
  44.126 -by (res_inst_tac [("p","b`(iterate m (step`b`g) x)")] trE 1);
  44.127 +by (res_inst_tac [("p","b$(iterate m (step$b$g) x)")] trE 1);
  44.128  by (Asm_simp_tac 1);
  44.129  by (Asm_simp_tac 1);
  44.130 -by (res_inst_tac [("s","xa`(iterate (Suc m) (step`b`g) x)")] trans 1);
  44.131 +by (res_inst_tac [("s","xa$(iterate (Suc m) (step$b$g) x)")] trans 1);
  44.132  by (etac spec 2);
  44.133  by (rtac cfun_arg_cong 1);
  44.134  by (rtac trans 1);
  44.135 @@ -141,12 +141,12 @@
  44.136  qed_spec_mp "loop_lemma5";
  44.137  
  44.138  
  44.139 -Goal "ALL k. b`(iterate k (step`b`g) x) ~= FF ==> while`b`g`x=UU";
  44.140 +Goal "ALL k. b$(iterate k (step$b$g) x) ~= FF ==> while$b$g$x=UU";
  44.141  by (res_inst_tac [("t","x")] (iterate_0 RS subst) 1);
  44.142  by (etac (loop_lemma5) 1);
  44.143  qed "loop_lemma6";
  44.144  
  44.145 -Goal "while`b`g`x ~= UU ==> EX k. b`(iterate k (step`b`g) x) = FF";
  44.146 +Goal "while$b$g$x ~= UU ==> EX k. b$(iterate k (step$b$g) x) = FF";
  44.147  by (blast_tac (claset() addIs [loop_lemma6]) 1);
  44.148  qed "loop_lemma7";
  44.149  
  44.150 @@ -156,10 +156,10 @@
  44.151  (* ------------------------------------------------------------------------- *)
  44.152  
  44.153  Goal
  44.154 -"[| (ALL y. INV y & b`y=TT & g`y ~= UU --> INV (g`y));\
  44.155 -\   (ALL y. INV y & b`y=FF --> Q y);\
  44.156 -\   INV x; while`b`g`x~=UU |] ==> Q (while`b`g`x)";
  44.157 -by (res_inst_tac [("P","%k. b`(iterate k (step`b`g) x)=FF")] exE 1);
  44.158 +"[| (ALL y. INV y & b$y=TT & g$y ~= UU --> INV (g$y));\
  44.159 +\   (ALL y. INV y & b$y=FF --> Q y);\
  44.160 +\   INV x; while$b$g$x~=UU |] ==> Q (while$b$g$x)";
  44.161 +by (res_inst_tac [("P","%k. b$(iterate k (step$b$g) x)=FF")] exE 1);
  44.162  by (etac loop_lemma7 1);
  44.163  by (stac (loop_lemma4) 1);
  44.164  by (atac 1);
  44.165 @@ -177,9 +177,9 @@
  44.166  val [premP,premI,premTT,premFF,premW] = Goal
  44.167  "[| P(x); \
  44.168  \   !!y. P y ==> INV y;\
  44.169 -\   !!y. [| INV y; b`y=TT; g`y~=UU|] ==> INV (g`y);\
  44.170 -\   !!y. [| INV y; b`y=FF|] ==> Q y;\
  44.171 -\   while`b`g`x ~= UU |] ==> Q (while`b`g`x)";
  44.172 +\   !!y. [| INV y; b$y=TT; g$y~=UU|] ==> INV (g$y);\
  44.173 +\   !!y. [| INV y; b$y=FF|] ==> Q y;\
  44.174 +\   while$b$g$x ~= UU |] ==> Q (while$b$g$x)";
  44.175  by (rtac loop_inv2 1);
  44.176  by (rtac (premP RS premI) 3);
  44.177  by (rtac premW 3);
    45.1 --- a/src/HOLCF/ex/Loop.thy	Tue Jan 09 15:32:27 2001 +0100
    45.2 +++ b/src/HOLCF/ex/Loop.thy	Tue Jan 09 15:36:30 2001 +0100
    45.3 @@ -14,9 +14,9 @@
    45.4  
    45.5  defs
    45.6  
    45.7 -  step_def      "step == (LAM b g x. If b`x then g`x else x fi)"
    45.8 -  while_def     "while == (LAM b g. fix`(LAM f x.
    45.9 -                   If b`x then f`(g`x) else x fi))"
   45.10 +  step_def      "step == (LAM b g x. If b$x then g$x else x fi)"
   45.11 +  while_def     "while == (LAM b g. fix$(LAM f x.
   45.12 +                   If b$x then f$(g$x) else x fi))"
   45.13  
   45.14  end
   45.15   
    46.1 --- a/src/HOLCF/ex/Stream.ML	Tue Jan 09 15:32:27 2001 +0100
    46.2 +++ b/src/HOLCF/ex/Stream.ML	Tue Jan 09 15:36:30 2001 +0100
    46.3 @@ -74,7 +74,7 @@
    46.4  
    46.5  section "stream_when";
    46.6  
    46.7 -Goal "stream_when`UU`s=UU";
    46.8 +Goal "stream_when$UU$s=UU";
    46.9  by (stream_case_tac "s" 1);
   46.10  by (ALLGOALS(asm_simp_tac (simpset() addsimps [strict_Rep_CFun1])));
   46.11  qed "stream_when_strictf";
   46.12 @@ -87,23 +87,23 @@
   46.13  section "ft & rt";
   46.14  
   46.15  (*
   46.16 -Goal "ft`s=UU --> s=UU";
   46.17 +Goal "ft$s=UU --> s=UU";
   46.18  by (stream_case_tac "s" 1);
   46.19  by (REPEAT (asm_simp_tac (simpset() addsimps stream.rews) 1));
   46.20  qed "stream_ft_lemma1";
   46.21  *)
   46.22  
   46.23 -Goal "s~=UU ==> ft`s~=UU";
   46.24 +Goal "s~=UU ==> ft$s~=UU";
   46.25  by (stream_case_tac "s" 1);
   46.26  by (Blast_tac 1);
   46.27  by (asm_simp_tac (simpset() addsimps stream.rews) 1);
   46.28  qed "ft_defin";
   46.29  
   46.30 -Goal "rt`s~=UU ==> s~=UU";
   46.31 +Goal "rt$s~=UU ==> s~=UU";
   46.32  by Auto_tac;
   46.33  qed "rt_strict_rev";
   46.34  
   46.35 -Goal "(ft`s)&&(rt`s)=s";
   46.36 +Goal "(ft$s)&&(rt$s)=s";
   46.37  by (stream_case_tac "s" 1);
   46.38  by (ALLGOALS (asm_simp_tac (simpset() addsimps stream.rews)));
   46.39  qed "surjectiv_scons";
   46.40 @@ -127,16 +127,16 @@
   46.41  
   46.42  section "stream_take";
   46.43  
   46.44 -Goal  "(LUB i. stream_take i`s) = s";
   46.45 -by (subgoal_tac "(LUB i. stream_take i`s) = fix`stream_copy`s" 1);
   46.46 +Goal  "(LUB i. stream_take i$s) = s";
   46.47 +by (subgoal_tac "(LUB i. stream_take i$s) = fix$stream_copy$s" 1);
   46.48  by (simp_tac (simpset() addsimps [fix_def2, stream.take_def,
   46.49                                    contlub_cfun_fun, chain_iterate]) 2);
   46.50  by (asm_full_simp_tac (simpset() addsimps [stream.reach]) 1);
   46.51  qed "stream_reach2";
   46.52  
   46.53 -Goal "chain (%i. stream_take i`s)";
   46.54 +Goal "chain (%i. stream_take i$s)";
   46.55  by (rtac chainI 1);
   46.56 -by (subgoal_tac "ALL i s. stream_take i`s << stream_take (Suc i)`s" 1);
   46.57 +by (subgoal_tac "ALL i s. stream_take i$s << stream_take (Suc i)$s" 1);
   46.58  by (Fast_tac 1);
   46.59  by (rtac allI 1);
   46.60  by (induct_tac "ia" 1);
   46.61 @@ -149,9 +149,9 @@
   46.62  
   46.63  
   46.64  Goalw [stream.take_def]
   46.65 -	"stream_take n`x = x ==> stream_take (Suc n)`x = x";
   46.66 +	"stream_take n$x = x ==> stream_take (Suc n)$x = x";
   46.67  by (rtac antisym_less 1);
   46.68 -by (subgoal_tac "iterate (Suc n) stream_copy UU`x << fix`stream_copy`x" 1);
   46.69 +by (subgoal_tac "iterate (Suc n) stream_copy UU$x << fix$stream_copy$x" 1);
   46.70  by (asm_full_simp_tac (simpset() addsimps [stream.reach]) 1);
   46.71  by (rtac monofun_cfun_fun 1);
   46.72  by (stac fix_def2 1);
   46.73 @@ -163,7 +163,7 @@
   46.74  
   46.75  (*
   46.76  Goal 
   46.77 - "ALL  s2. stream_take n`s2 = s2 --> stream_take (Suc n)`s2=s2";
   46.78 + "ALL  s2. stream_take n$s2 = s2 --> stream_take (Suc n)$s2=s2";
   46.79  by (induct_tac "n" 1);
   46.80  by (simp_tac (simpset() addsimps stream_rews) 1);
   46.81  by (strip_tac 1);
   46.82 @@ -174,7 +174,7 @@
   46.83  by (asm_simp_tac (simpset() addsimps stream_rews) 1);
   46.84  by (asm_simp_tac (simpset() addsimps stream_rews) 1);
   46.85  by (strip_tac 1 );
   46.86 -by (subgoal_tac "stream_take n1`xs = xs" 1);
   46.87 +by (subgoal_tac "stream_take n1$xs = xs" 1);
   46.88  by (rtac ((hd stream_inject) RS conjunct2) 2);
   46.89  by (atac 4);
   46.90  by (atac 2);
   46.91 @@ -185,7 +185,7 @@
   46.92  *)
   46.93  
   46.94  Goal 
   46.95 - "ALL x xs. x~=UU --> stream_take n`(x && xs) = x && xs --> stream_take n`xs=xs";
   46.96 + "ALL x xs. x~=UU --> stream_take n$(x && xs) = x && xs --> stream_take n$xs=xs";
   46.97  by (induct_tac "n" 1);
   46.98  by (Asm_simp_tac 1);
   46.99  by (strip_tac 1);
  46.100 @@ -201,7 +201,7 @@
  46.101  qed_spec_mp "stream_take_lemma3";
  46.102  
  46.103  Goal 
  46.104 - "ALL x xs. stream_take n`xs=xs --> stream_take (Suc n)`(x && xs) = x && xs";
  46.105 + "ALL x xs. stream_take n$xs=xs --> stream_take (Suc n)$(x && xs) = x && xs";
  46.106  by (induct_tac "n" 1);
  46.107  by Auto_tac;  
  46.108  qed_spec_mp "stream_take_lemma4";
  46.109 @@ -232,7 +232,7 @@
  46.110  "[| P UU;\
  46.111  \   !! x    .    x ~= UU                  ==> P (x      && UU); \
  46.112  \   !! y z s. [| y ~= UU; z ~= UU; P s |] ==> P (y && z && s )  \
  46.113 -\   |] ==> !s. P (stream_take n`s)";
  46.114 +\   |] ==> !s. P (stream_take n$s)";
  46.115  by (res_inst_tac [("n","n")] nat_induct2 1);
  46.116  by (asm_simp_tac (simpset() addsimps [major]) 1);
  46.117  by (rtac allI 1);
  46.118 @@ -275,7 +275,7 @@
  46.119  
  46.120  
  46.121  Goalw [stream.bisim_def]
  46.122 -"!s1 s2. R s1 s2 --> ft`s1 = ft`s2 &  R (rt`s1) (rt`s2) ==> stream_bisim R";
  46.123 +"!s1 s2. R s1 s2 --> ft$s1 = ft$s2 &  R (rt$s1) (rt$s2) ==> stream_bisim R";
  46.124  by (strip_tac 1);
  46.125  by (etac allE 1);
  46.126  by (etac allE 1);
  46.127 @@ -288,21 +288,21 @@
  46.128  by (rtac disjI2 1);
  46.129  by (rtac disjE 1);
  46.130  by (etac (de_Morgan_conj RS subst) 1);
  46.131 -by (res_inst_tac [("x","ft`x")] exI 1);
  46.132 -by (res_inst_tac [("x","rt`x")] exI 1);
  46.133 -by (res_inst_tac [("x","rt`x'")] exI 1);
  46.134 +by (res_inst_tac [("x","ft$x")] exI 1);
  46.135 +by (res_inst_tac [("x","rt$x")] exI 1);
  46.136 +by (res_inst_tac [("x","rt$x'")] exI 1);
  46.137  by (rtac conjI 1);
  46.138  by (etac ft_defin 1);
  46.139  by (asm_simp_tac (simpset() addsimps stream.rews addsimps [surjectiv_scons]) 1);
  46.140 -by (eres_inst_tac [("s","ft`x"),("t","ft`x'")] subst 1);
  46.141 +by (eres_inst_tac [("s","ft$x"),("t","ft$x'")] subst 1);
  46.142  by (simp_tac (simpset() addsimps stream.rews addsimps [surjectiv_scons]) 1);
  46.143 -by (res_inst_tac [("x","ft`x'")] exI 1);
  46.144 -by (res_inst_tac [("x","rt`x")] exI 1);
  46.145 -by (res_inst_tac [("x","rt`x'")] exI 1);
  46.146 +by (res_inst_tac [("x","ft$x'")] exI 1);
  46.147 +by (res_inst_tac [("x","rt$x")] exI 1);
  46.148 +by (res_inst_tac [("x","rt$x'")] exI 1);
  46.149  by (rtac conjI 1);
  46.150  by (etac ft_defin 1);
  46.151  by (asm_simp_tac (simpset() addsimps stream.rews addsimps [surjectiv_scons]) 1);
  46.152 -by (res_inst_tac [("s","ft`x"),("t","ft`x'")] ssubst 1);
  46.153 +by (res_inst_tac [("s","ft$x"),("t","ft$x'")] ssubst 1);
  46.154  by (etac sym 1);
  46.155  by (simp_tac (simpset() addsimps stream.rews addsimps [surjectiv_scons]) 1);
  46.156  qed "stream_coind_lemma2";
  46.157 @@ -332,7 +332,7 @@
  46.158  by (blast_tac (claset() addIs [stream_take_lemma3]) 1);
  46.159  qed "stream_finite_lemma2";
  46.160  
  46.161 -Goal "stream_finite (rt`s) = stream_finite s";
  46.162 +Goal "stream_finite (rt$s) = stream_finite s";
  46.163  by (stream_case_tac "s" 1);
  46.164  by (simp_tac (simpset() addsimps [stream_finite_UU]) 1);
  46.165  by (Asm_simp_tac 1);
    47.1 --- a/src/HOLCF/ex/loeckx.ML	Tue Jan 09 15:32:27 2001 +0100
    47.2 +++ b/src/HOLCF/ex/loeckx.ML	Tue Jan 09 15:36:30 2001 +0100
    47.3 @@ -19,16 +19,16 @@
    47.4  Since we already proved the theorem
    47.5  
    47.6  val cont_lubcfun = prove_goal Cfun2.thy 
    47.7 -        "chain ?F ==> cont (%x. lub (range (%j. ?F j`x)))"
    47.8 +        "chain ?F ==> cont (%x. lub (range (%j. ?F j$x)))"
    47.9  
   47.10  
   47.11  it suffices to prove:
   47.12  
   47.13 -Ifix  = (%f.lub (range (%j. (LAM f. iterate j f UU)`f)))
   47.14 +Ifix  = (%f.lub (range (%j. (LAM f. iterate j f UU)$f)))
   47.15  
   47.16  and 
   47.17  
   47.18 -cont (%f.lub (range (%j. (LAM f. iterate j f UU)`f)))
   47.19 +cont (%f.lub (range (%j. (LAM f. iterate j f UU)$f)))
   47.20  
   47.21  Note that if we use the term 
   47.22  
   47.23 @@ -40,15 +40,15 @@
   47.24  
   47.25  Goal "cont(Ifix)";
   47.26  by (res_inst_tac 
   47.27 - [("t","Ifix"),("s","(%f. lub(range(%j.(LAM f. iterate j f UU)`f)))")]
   47.28 + [("t","Ifix"),("s","(%f. lub(range(%j.(LAM f. iterate j f UU)$f)))")]
   47.29    ssubst 1);
   47.30  by (rtac ext 1);
   47.31  by (rewtac Ifix_def );
   47.32  by (subgoal_tac 
   47.33 -  "range(% i. iterate i f UU) = range(%j.(LAM f. iterate j f UU)`f)" 1);
   47.34 +  "range(% i. iterate i f UU) = range(%j.(LAM f. iterate j f UU)$f)" 1);
   47.35  by (etac arg_cong 1);
   47.36  by (subgoal_tac 
   47.37 -        "(% i. iterate i f UU) = (%j.(LAM f. iterate j f UU)`f)" 1);
   47.38 +        "(% i. iterate i f UU) = (%j.(LAM f. iterate j f UU)$f)" 1);
   47.39  by (etac arg_cong 1);
   47.40  by (rtac ext 1);
   47.41  by (stac beta_cfun 1);
   47.42 @@ -70,19 +70,19 @@
   47.43  
   47.44  (* the proof in little steps *)
   47.45  
   47.46 -Goal "(% i. iterate i f UU) = (%j.(LAM f. iterate j f UU)`f)";
   47.47 +Goal "(% i. iterate i f UU) = (%j.(LAM f. iterate j f UU)$f)";
   47.48  by (rtac ext 1);
   47.49  by (simp_tac (simpset() addsimps [beta_cfun, cont2cont_CF1L, cont_iterate]) 1);
   47.50  qed "fix_lemma1";
   47.51  
   47.52 -Goal "Ifix = (%f. lub(range(%j.(LAM f. iterate j f UU)`f)))";
   47.53 +Goal "Ifix = (%f. lub(range(%j.(LAM f. iterate j f UU)$f)))";
   47.54  by (rtac ext 1);
   47.55  by (simp_tac (simpset() addsimps [Ifix_def, fix_lemma1]) 1);
   47.56  qed "fix_lemma2";
   47.57  
   47.58  (*
   47.59  - cont_lubcfun;
   47.60 -val it = "chain ?F ==> cont (%x. lub (range (%j. ?F j`x)))" : thm   
   47.61 +val it = "chain ?F ==> cont (%x. lub (range (%j. ?F j$x)))" : thm   
   47.62  
   47.63  *)
   47.64