src/HOLCF/FOCUS/Buffer_adm.ML
changeset 12484 7ad150f5fc10
parent 11704 3c50a2cd6f00
child 13454 01e2496dee05
     1.1 --- a/src/HOLCF/FOCUS/Buffer_adm.ML	Wed Dec 12 19:22:21 2001 +0100
     1.2 +++ b/src/HOLCF/FOCUS/Buffer_adm.ML	Wed Dec 12 20:37:31 2001 +0100
     1.3 @@ -86,7 +86,7 @@
     1.4   (K [
     1.5  	rtac (BufAC_Cmt_unfold RS iffD2) 1,
     1.6  	strip_tac 1,
     1.7 -	forward_tac [Buf_f_d_req] 1,
     1.8 +	ftac Buf_f_d_req 1,
     1.9  	auto_tac (claset() addEs [BufAC_Asm_cong RS subst],simpset())]);
    1.10  
    1.11  (*adm_BufAC_Asm*)
    1.12 @@ -118,7 +118,7 @@
    1.13  by (strip_tac 1);
    1.14  by (stac BufAC_Cmt_F_def3 1);
    1.15  by (dres_inst_tac [("P","%x. x")] (BufAC_Cmt_F_def3 RS subst) 1);
    1.16 -by (Safe_tac);
    1.17 +by Safe_tac;
    1.18  by (   etac Buf_f_empty 1);
    1.19  by (  etac Buf_f_d 1);
    1.20  by ( dtac Buf_f_d_req 1);
    1.21 @@ -215,8 +215,8 @@
    1.22  (**** new approach for admissibility, reduces itself to absurdity *************)
    1.23  
    1.24  Goal "adm (\\<lambda>x. x\\<in>BufAC_Asm)";
    1.25 -by(rtac def_gfp_admI 1);
    1.26 -by(rtac BufAC_Asm_def 1);
    1.27 +by (rtac def_gfp_admI 1);
    1.28 +by (rtac BufAC_Asm_def 1);
    1.29  b y Safe_tac;
    1.30  b y rewtac BufAC_Asm_F_def;
    1.31  b y Safe_tac;
    1.32 @@ -238,7 +238,7 @@
    1.33  b y Clarsimp_tac 1;
    1.34  b y simp_tac (HOL_basic_ss addsimps (ex_simps@all_simps RL[sym])) 1;
    1.35  b y res_inst_tac [("x","Xa")] exI 1;
    1.36 -br allI 1;
    1.37 +by (rtac allI 1);
    1.38  b y rotate_tac ~1 1;
    1.39  b y eres_inst_tac [("x","i")] allE 1;
    1.40  b y Clarsimp_tac 1;
    1.41 @@ -271,8 +271,8 @@
    1.42  qed "adm_non_BufAC_Asm";
    1.43  
    1.44  Goal "f \\<in> BufEq \\<Longrightarrow> adm (\\<lambda>u. u \\<in> BufAC_Asm \\<longrightarrow> (u, f\\<cdot>u) \\<in> BufAC_Cmt)";
    1.45 -by(rtac triv_admI 1);
    1.46 -by(Clarify_tac 1);
    1.47 -by(eatac Buf_Eq_imp_AC_lemma 1 1); 
    1.48 +by (rtac triv_admI 1);
    1.49 +by (Clarify_tac 1);
    1.50 +by (eatac Buf_Eq_imp_AC_lemma 1 1); 
    1.51        (* this is what we originally aimed to show, using admissibilty :-( *)
    1.52  qed "adm_BufAC";