expandshort

--- a/src/HOL/Finite.ML	Wed Mar 01 12:26:28 2000 +0100
+++ b/src/HOL/Finite.ML	Wed Mar 01 15:00:21 2000 +0100
@@ -178,9 +178,9 @@
 qed "finite_Prod_UNIV";
 
 Goal "finite (UNIV :: ('a::finite * 'b::finite) set)";
-br (finite_Prod_UNIV) 1;
-br finite 1;
-br finite 1;
+by (rtac (finite_Prod_UNIV) 1);
+by (rtac finite 1);
+by (rtac finite 1);
 qed "finite_Prod";
 
 (** The powerset of a finite set **)
@@ -833,7 +833,7 @@
 by (res_inst_tac [("f", "%s. s - {x}"), ("g","insert x")] card_bij_eq 1);
 by (res_inst_tac [("B","Pow(insert x M)")] finite_subset 1);
 by (res_inst_tac [("B","Pow(M)")] finite_subset 3);
-by(REPEAT(Fast_tac 1));
+by (REPEAT(Fast_tac 1));
 (* arity *)
 by (auto_tac (claset() addSEs [equalityE], simpset() addsimps [inj_on_def]));
 by (stac Diff_insert0 1);

--- a/src/HOL/Prod.ML	Wed Mar 01 12:26:28 2000 +0100
+++ b/src/HOL/Prod.ML	Wed Mar 01 15:00:21 2000 +0100
@@ -142,7 +142,7 @@
 qed "split_weak_cong";
 
 Goal "(%u. ? x y. u = (x, y) & P (x, y)) = P"; 
-br ext 1;
+by (rtac ext 1);
 by (Fast_tac 1);
 qed "split_eta_SetCompr";
 Addsimps [split_eta_SetCompr];

--- a/src/HOL/Trancl.ML	Wed Mar 01 12:26:28 2000 +0100
+++ b/src/HOL/Trancl.ML	Wed Mar 01 15:00:21 2000 +0100
@@ -102,14 +102,11 @@
 (*** More r^* equations and inclusions ***)
 
 Goal "(r^*)^* = r^*";
-by (rtac set_ext 1);
-by (res_inst_tac [("p","x")] PairE 1);
-by (hyp_subst_tac 1);
-by (rtac iffI 1);
+by Auto_tac;
+by (etac r_into_rtrancl 2);
 by (etac rtrancl_induct 1);
 by (rtac rtrancl_refl 1);
 by (blast_tac (claset() addIs [rtrancl_trans]) 1);
-by (etac r_into_rtrancl 1);
 qed "rtrancl_idemp";
 Addsimps [rtrancl_idemp];
 
@@ -143,14 +140,14 @@
 Addsimps [rtrancl_reflcl];
 
 Goal "(r - Id)^* = r^*";
-br sym 1;
-br rtrancl_subset 1;
+by (rtac sym 1);
+by (rtac rtrancl_subset 1);
  by (Blast_tac 1);
 by (Clarify_tac 1);
-by(rename_tac "a b" 1);
-by(case_tac "a=b" 1);
+by (rename_tac "a b" 1);
+by (case_tac "a=b" 1);
  by (Blast_tac 1);
-by(blast_tac (claset() addSIs [r_into_rtrancl]) 1);
+by (blast_tac (claset() addSIs [r_into_rtrancl]) 1);
 qed "rtrancl_r_diff_Id";
 
 Goal "(x,y) : (r^-1)^* ==> (x,y) : (r^*)^-1";