src/HOL/ex/LocaleGroup.ML

--- a/src/HOL/ex/LocaleGroup.ML	Fri Aug 14 12:02:35 1998 +0200
+++ b/src/HOL/ex/LocaleGroup.ML	Fri Aug 14 12:03:01 1998 +0200
@@ -19,10 +19,10 @@
 (* Mit dieser Def ist es halt schwierig *)
 goal LocaleGroup.thy "op # : carrier G -> carrier G -> carrier G";
 by (res_inst_tac [("t","op #")] ssubst 1);
-br ext 1;
-br ext 1;
-br meta_eq_to_obj_eq 1;
-br (thm "binop_def") 1;
+by (rtac ext 1);
+by (rtac ext 1);
+by (rtac meta_eq_to_obj_eq 1);
+by (rtac (thm "binop_def") 1);
 by (Asm_full_simp_tac 1);
 val binop_funcset = result();
 
@@ -32,9 +32,9 @@
 
 goal LocaleGroup.thy "inv : carrier G -> carrier G";
 by (res_inst_tac [("t","inv")] ssubst 1);
-br ext 1;
-br meta_eq_to_obj_eq 1;
-br (thm "inv_def") 1;
+by (rtac ext 1);
+by (rtac meta_eq_to_obj_eq 1);
+by (rtac (thm "inv_def") 1);
 by (Asm_full_simp_tac 1);
 val inv_funcset = result();
 
@@ -71,27 +71,27 @@
 (* remarkable: In the following step the use of e_ax1 instead of unit_ax1
    is better! It doesn't produce G: Group as subgoal and the nice syntax stays *)
 by (res_inst_tac [("P","%r. r = z")] (e_ax1 RS subst) 1);
-ba 1;
+by (assume_tac 1);
 (* great: we can use the nice syntax even in res_inst_tac *)
 by (res_inst_tac [("P","%r. r # y = z")] subst 1);
 by (res_inst_tac [("x","x")] inv_ax2 1);
-ba 1;
-br (binop_assoc RS ssubst) 1;
-br inv_closed 1;
-ba 1;
-ba 1;
-ba 1;
-be ssubst 1;
-br (binop_assoc RS subst) 1;
-br inv_closed 1;
-ba 1;
-ba 1;
-ba 1;
-br (inv_ax2 RS ssubst) 1;
-ba 1;
-br (e_ax1 RS ssubst) 1;
-ba 1;
-br refl 1;
+by (assume_tac 1);
+by (stac binop_assoc 1);
+by (rtac inv_closed 1);
+by (assume_tac 1);
+by (assume_tac 1);
+by (assume_tac 1);
+by (etac ssubst 1);
+by (rtac (binop_assoc RS subst) 1);
+by (rtac inv_closed 1);
+by (assume_tac 1);
+by (assume_tac 1);
+by (assume_tac 1);
+by (stac inv_ax2 1);
+by (assume_tac 1);
+by (stac e_ax1 1);
+by (assume_tac 1);
+by (rtac refl 1);
 val left_cancellation = result();
 
 
@@ -105,57 +105,57 @@
 by (fold_goals_tac [thm "inv_def"]);
 by (fast_tac (claset() addSEs [inv_closed]) 1);
 by (afs [binop_closed, e_closed] 1);
-ba 1;
-br (binop_assoc RS subst) 1;
+by (assume_tac 1);
+by (rtac (binop_assoc RS subst) 1);
 by (fast_tac (claset() addSEs [inv_closed]) 1);
-ba 1;
-br (e_closed) 1;
-br (inv_ax2 RS ssubst) 1;
-ba 1;
-br (e_ax1 RS ssubst) 1;
-br e_closed 1;
-br refl 1;
+by (assume_tac 1);
+by (rtac (e_closed) 1);
+by (stac inv_ax2 1);
+by (assume_tac 1);
+by (stac e_ax1 1);
+by (rtac e_closed 1);
+by (rtac refl 1);
 val e_ax2 = result();
 
 goal LocaleGroup.thy "!! x. [| x: carrier G; x # x = x |] ==> x = e";
 by (forw_inst_tac [("P","%y. x # x = y")] (e_ax2 RS forw_subst) 1);
-ba 1;
+by (assume_tac 1);
 by (res_inst_tac [("x","x")] left_cancellation 1);
-ba 1;
-ba 1;
-br e_closed 1;
-ba 1;
+by (assume_tac 1);
+by (assume_tac 1);
+by (rtac e_closed 1);
+by (assume_tac 1);
 val idempotent_e = result();
 
 goal LocaleGroup.thy  "!! x. x: carrier G ==> x # (x -|) = e";
-br idempotent_e 1;
+by (rtac idempotent_e 1);
 by (afs [binop_closed,inv_closed] 1);
-br (binop_assoc RS ssubst) 1;
-ba 1;
+by (stac binop_assoc 1);
+by (assume_tac 1);
 by (afs [inv_closed] 1);
 by (afs [binop_closed,inv_closed] 1);
 by (res_inst_tac [("t","x -| # x # x -|")] subst 1);
-br binop_assoc 1;
+by (rtac binop_assoc 1);
 by (afs [inv_closed] 1);
-ba 1;
+by (assume_tac 1);
 by (afs [inv_closed] 1);
-br (inv_ax2 RS ssubst) 1;
-ba 1;
-br (e_ax1 RS ssubst) 1;
+by (stac inv_ax2 1);
+by (assume_tac 1);
+by (stac e_ax1 1);
 by (afs [inv_closed] 1);
-br refl 1;
+by (rtac refl 1);
 val inv_ax1 = result();
 
 
 goal LocaleGroup.thy "!! x y. [| x: carrier G; y: carrier G; \
 \                     x # y = e |] ==> y = x -|";
 by (res_inst_tac [("x","x")] left_cancellation 1);
-ba 1;
-ba 1;
+by (assume_tac 1);
+by (assume_tac 1);
 by (afs [inv_closed] 1);
-br (inv_ax1 RS ssubst) 1;
-ba 1;
-ba 1;
+by (stac inv_ax1 1);
+by (assume_tac 1);
+by (assume_tac 1);
 val inv_unique = result();
 
 goal LocaleGroup.thy "!! x. x : carrier G ==> x -| -| = x";
@@ -163,19 +163,19 @@
 by (fold_goals_tac [thm "inv_def"]);
 by (afs [inv_closed] 1);
 by (afs [inv_closed] 1);
-ba 1;
+by (assume_tac 1);
 by (afs [inv_ax1,inv_ax2,e_ax1,e_ax2,e_closed,inv_closed,binop_closed] 1);
 val inv_inv = result();
 
 goal LocaleGroup.thy "!! x y. [| x : carrier G; y : carrier G |]\
 \           ==> (x # y) -| = y -| # x -|";
-br sym 1;
-br inv_unique 1;
+by (rtac sym 1);
+by (rtac inv_unique 1);
 by (afs [binop_closed] 1);
 by (afs [inv_closed,binop_closed] 1);
 by (afs [binop_assoc,inv_closed,binop_closed] 1);
 by (res_inst_tac [("x1","y")] (binop_assoc RS subst) 1);
-ba 1;
+by (assume_tac 1);
 by (afs [inv_closed] 1);
 by (afs [inv_closed] 1);
 by (afs [inv_ax1,inv_ax2,e_ax1,e_ax2,e_closed,inv_closed,binop_closed] 1);
@@ -185,15 +185,15 @@
 goal LocaleGroup.thy "!! x y z. [| x : carrier G; y : carrier G;\
 \ z : carrier G; y # x =  z # x|] ==> y = z";
 by (res_inst_tac [("P","%r. r = z")] (e_ax2 RS subst) 1);
-ba 1;
+by (assume_tac 1);
 by (res_inst_tac [("P","%r. y # r = z")] subst 1);
-br inv_ax1 1;
-ba 1;
-br (binop_assoc RS subst) 1;
-ba 1;
-ba 1;
+by (rtac inv_ax1 1);
+by (assume_tac 1);
+by (rtac (binop_assoc RS subst) 1);
+by (assume_tac 1);
+by (assume_tac 1);
 by (afs [inv_closed] 1);
-be ssubst 1;
+by (etac ssubst 1);
 by (afs [binop_assoc,inv_closed,inv_ax1,e_ax2] 1);
 val right_cancellation = result();