src/HOLCF/IOA/meta_theory/CompoScheds.ML
changeset 4477 b3e5857d8d99
parent 4423 a129b817b58a
child 4520 d430a1b34928
     1.1 --- a/src/HOLCF/IOA/meta_theory/CompoScheds.ML	Tue Dec 23 11:56:09 1997 +0100
     1.2 +++ b/src/HOLCF/IOA/meta_theory/CompoScheds.ML	Wed Dec 24 10:02:30 1997 +0100
     1.3 @@ -115,7 +115,7 @@
     1.4  by (simp_tac (simpset() addsimps [mkex_def] 
     1.5                         setloop (split_tac [expand_if]) ) 1);
     1.6  by (cut_inst_tac [("exA","a>>exA")] mkex2_cons_1 1);
     1.7 -by (Auto_tac());
     1.8 +by Auto_tac;
     1.9  qed"mkex_cons_1";
    1.10  
    1.11  goal thy "!!x.[| x~:act A; x:act B |] \
    1.12 @@ -124,7 +124,7 @@
    1.13  by (simp_tac (simpset() addsimps [mkex_def] 
    1.14                         setloop (split_tac [expand_if]) ) 1);
    1.15  by (cut_inst_tac [("exB","b>>exB")] mkex2_cons_2 1);
    1.16 -by (Auto_tac());
    1.17 +by Auto_tac;
    1.18  qed"mkex_cons_2";
    1.19  
    1.20  goal thy "!!x.[| x:act A; x:act B |]  \
    1.21 @@ -133,7 +133,7 @@
    1.22  by (simp_tac (simpset() addsimps [mkex_def] 
    1.23                         setloop (split_tac [expand_if]) ) 1);
    1.24  by (cut_inst_tac [("exB","b>>exB"),("exA","a>>exA")] mkex2_cons_3 1);
    1.25 -by (Auto_tac());
    1.26 +by Auto_tac;
    1.27  qed"mkex_cons_3";
    1.28  
    1.29  Delsimps [mkex2_UU,mkex2_nil,mkex2_cons_1,mkex2_cons_2,mkex2_cons_3];
    1.30 @@ -364,7 +364,7 @@
    1.31  by (Seq_induct_tac "x" [] 1);
    1.32  by (Seq_case_simp_tac "y" 2);
    1.33  by (pair_tac "a" 1);
    1.34 -by (Auto_tac());
    1.35 +by Auto_tac;
    1.36  
    1.37  *)
    1.38