src/HOLCF/IOA/meta_theory/Abstraction.ML
changeset 10835 f4745d77e620
parent 7499 23e090051cb8
child 12218 6597093b77e7
     1.1 --- a/src/HOLCF/IOA/meta_theory/Abstraction.ML	Tue Jan 09 15:32:27 2001 +0100
     1.2 +++ b/src/HOLCF/IOA/meta_theory/Abstraction.ML	Tue Jan 09 15:36:30 2001 +0100
     1.3 @@ -181,7 +181,7 @@
     1.4     that is to special Map Lemma *)
     1.5  Goalw [cex_abs_def,mk_trace_def,filter_act_def]
     1.6    "ext C = ext A \
     1.7 -\        ==> mk_trace C`xs = mk_trace A`(snd (cex_abs f (s,xs)))";
     1.8 +\        ==> mk_trace C$xs = mk_trace A$(snd (cex_abs f (s,xs)))";
     1.9  by (Asm_full_simp_tac 1);
    1.10  by (pair_induct_tac "xs" [] 1);
    1.11  qed"traces_coincide_abs";
    1.12 @@ -383,11 +383,11 @@
    1.13  
    1.14  (* FIX: NAch Sequence.ML bringen *)
    1.15  
    1.16 -Goal "(Map f`s = nil) = (s=nil)";
    1.17 +Goal "(Map f$s = nil) = (s=nil)";
    1.18  by (Seq_case_simp_tac "s" 1);
    1.19  qed"Mapnil";
    1.20  
    1.21 -Goal "(Map f`s = UU) = (s=UU)";
    1.22 +Goal "(Map f$s = UU) = (s=UU)";
    1.23  by (Seq_case_simp_tac "s" 1);
    1.24  qed"MapUU";
    1.25  
    1.26 @@ -400,7 +400,7 @@
    1.27  by Auto_tac;
    1.28  by (asm_full_simp_tac (simpset() addsimps [Mapnil])1);
    1.29  by (asm_full_simp_tac (simpset() addsimps [MapUU])1);
    1.30 -by (res_inst_tac [("x","Map (%(s,a,t). (h s,a, h t))`s1")] exI 1);
    1.31 +by (res_inst_tac [("x","Map (%(s,a,t). (h s,a, h t))$s1")] exI 1);
    1.32  by (asm_full_simp_tac (simpset() addsimps [Map2Finite,MapConc])1);
    1.33  qed"cex_absSeq_tsuffix";
    1.34  
    1.35 @@ -433,7 +433,7 @@
    1.36  (* ------------------ Next ----------------------------*)
    1.37  
    1.38  Goal 
    1.39 -"(TL`(ex2seq (cex_abs h ex))=UU) = (TL`(ex2seq ex)=UU)";
    1.40 +"(TL$(ex2seq (cex_abs h ex))=UU) = (TL$(ex2seq ex)=UU)";
    1.41  by (pair_tac "ex" 1);
    1.42  by (Seq_case_simp_tac "y" 1);
    1.43  by (pair_tac "a" 1);
    1.44 @@ -442,7 +442,7 @@
    1.45  qed"TL_ex2seq_UU";
    1.46  
    1.47  Goal 
    1.48 -"(TL`(ex2seq (cex_abs h ex))=nil) = (TL`(ex2seq ex)=nil)";
    1.49 +"(TL$(ex2seq (cex_abs h ex))=nil) = (TL$(ex2seq ex)=nil)";
    1.50  by (pair_tac "ex" 1);
    1.51  by (Seq_case_simp_tac "y" 1);
    1.52  by (pair_tac "a" 1);
    1.53 @@ -451,7 +451,7 @@
    1.54  qed"TL_ex2seq_nil";
    1.55  
    1.56  (* FIX: put to Sequence Lemmas *)
    1.57 -Goal "Map f`(TL`s) = TL`(Map f`s)";
    1.58 +Goal "Map f$(TL$s) = TL$(Map f$s)";
    1.59  by (Seq_induct_tac "s" [] 1);
    1.60  qed"MapTL";
    1.61  
    1.62 @@ -459,13 +459,13 @@
    1.63    properties carry over *)
    1.64  
    1.65  Goalw [cex_absSeq_def]
    1.66 -"cex_absSeq h (TL`s) = (TL`(cex_absSeq h s))";
    1.67 +"cex_absSeq h (TL$s) = (TL$(cex_absSeq h s))";
    1.68  by (simp_tac (simpset() addsimps [MapTL]) 1);
    1.69  qed"cex_absSeq_TL";
    1.70  
    1.71  (* important property of ex2seq: can be shiftet, as defined "pointwise" *)
    1.72  
    1.73 -Goal "[| (snd ex)~=UU ; (snd ex)~=nil |] ==> (? ex'. TL`(ex2seq ex) = ex2seq ex')";
    1.74 +Goal "[| (snd ex)~=UU ; (snd ex)~=nil |] ==> (? ex'. TL$(ex2seq ex) = ex2seq ex')";
    1.75  by (pair_tac "ex" 1);
    1.76  by (Seq_case_simp_tac "y" 1);
    1.77  by (pair_tac "a" 1);
    1.78 @@ -473,7 +473,7 @@
    1.79  qed"TLex2seq";
    1.80  
    1.81   
    1.82 -Goal "(TL`(ex2seq ex)~=nil) = ((snd ex)~=nil & (snd ex)~=UU)";
    1.83 +Goal "(TL$(ex2seq ex)~=nil) = ((snd ex)~=nil & (snd ex)~=UU)";
    1.84  by (pair_tac "ex" 1);
    1.85  by (Seq_case_simp_tac "y" 1);
    1.86  by (pair_tac "a" 1);