src/HOLCF/FOCUS/Buffer_adm.ML
changeset 11655 923e4d0d36d5
parent 11378 5c84a5ca3a21
child 11701 3d51fbf81c17
     1.1 --- a/src/HOLCF/FOCUS/Buffer_adm.ML	Wed Oct 03 20:54:05 2001 +0200
     1.2 +++ b/src/HOLCF/FOCUS/Buffer_adm.ML	Wed Oct 03 20:54:16 2001 +0200
     1.3 @@ -15,7 +15,7 @@
     1.4      "a\\<leadsto>b\\<leadsto>s:BufAC_Asm ==> ? d. a=Md d & b=\\<bullet> & s:BufAC_Asm" BufAC_Asm_unfold;
     1.5  
     1.6  val BufAC_Asm_F_def3 = prove_goalw thy [BufAC_Asm_F_def] 
     1.7 - "s:BufAC_Asm_F A = (s=<> | \
     1.8 + "(s:BufAC_Asm_F A) = (s=<> | \
     1.9  \ (? d. ft\\<cdot>s=Def(Md d)) & (rt\\<cdot>s=<> | ft\\<cdot>(rt\\<cdot>s)=Def \\<bullet> & rt\\<cdot>(rt\\<cdot>s):A))" (K [
    1.10  	Auto_tac]);
    1.11  
    1.12 @@ -24,7 +24,7 @@
    1.13  qed "cont_BufAC_Asm_F";
    1.14  
    1.15  val BufAC_Cmt_F_def3 = prove_goalw thy [BufAC_Cmt_F_def] 
    1.16 - "(s,t):BufAC_Cmt_F C = (!d x.\
    1.17 + "((s,t):BufAC_Cmt_F C) = (!d x.\
    1.18  \   (s = <>       --> t = <>                   ) & \
    1.19  \   (s = Md d\\<leadsto><>  --> t = <>                   ) & \
    1.20  \   (s = Md d\\<leadsto>\\<bullet>\\<leadsto>x --> ft\\<cdot>t = Def d & (x,rt\\<cdot>t):C))" (fn _=> [
    1.21 @@ -166,7 +166,7 @@
    1.22  by (EVERY[stac BufAC_Asm_cong 1, atac 1, atac 3, atac 1, atac 1]);
    1.23  qed "BufAC_Cmt_2stream_monoP";
    1.24  
    1.25 -Goalw [BufAC_Cmt_def] "x\\<in>BufAC_Cmt = (\\<forall>n. x\\<in>down_iterate BufAC_Cmt_F n)";
    1.26 +Goalw [BufAC_Cmt_def] "(x\\<in>BufAC_Cmt) = (\\<forall>n. x\\<in>down_iterate BufAC_Cmt_F n)";
    1.27  by (stac (cont_BufAC_Cmt_F RS INTER_down_iterate_is_gfp) 1);
    1.28  by (Fast_tac 1);
    1.29  qed "BufAC_Cmt_iterate_all";