removal of batch style, and tidying

--- a/src/HOL/Induct/Multiset.ML	Thu Jul 06 13:35:40 2000 +0200
+++ b/src/HOL/Induct/Multiset.ML	Thu Jul 06 15:01:52 2000 +0200
@@ -82,9 +82,11 @@
 by (simp_tac (simpset() addsimps add_ac) 1);
 qed "union_assoc";
 
-qed_goal "union_lcomm" thy "M+(N+K) = N+((M+K)::'a multiset)"
- (fn _ => [rtac (union_commute RS trans) 1, rtac (union_assoc RS trans) 1,
-           rtac (union_commute RS arg_cong) 1]);
+Goal "M+(N+K) = N+((M+K)::'a multiset)";
+by (rtac (union_commute RS trans) 1);
+by (rtac (union_assoc RS trans) 1);
+by (rtac (union_commute RS arg_cong) 1);
+qed "union_lcomm";
 
 bind_thms ("union_ac", [union_assoc, union_commute, union_lcomm]);
 

--- a/src/HOL/Real/PReal.ML	Thu Jul 06 13:35:40 2000 +0200
+++ b/src/HOL/Real/PReal.ML	Thu Jul 06 15:01:52 2000 +0200
@@ -275,10 +275,11 @@
 by (auto_tac (claset() addSIs [exI],simpset() addsimps prat_add_ac));
 qed "preal_add_assoc";
 
-qed_goal "preal_add_left_commute" thy
-    "(z1::preal) + (z2 + z3) = z2 + (z1 + z3)"
- (fn _ => [rtac (preal_add_commute RS trans) 1, rtac (preal_add_assoc RS trans) 1,
-           rtac (preal_add_commute RS arg_cong) 1]);
+Goal "(z1::preal) + (z2 + z3) = z2 + (z1 + z3)";
+by (rtac (preal_add_commute RS trans) 1);
+by (rtac (preal_add_assoc RS trans) 1);
+by (rtac (preal_add_commute RS arg_cong) 1);
+qed "preal_add_left_commute";
 
 (* Positive Reals addition is an AC operator *)
 bind_thms ("preal_add_ac", [preal_add_assoc, preal_add_commute, preal_add_left_commute]);
@@ -360,11 +361,11 @@
 by (auto_tac (claset() addSIs [exI],simpset() addsimps prat_mult_ac));
 qed "preal_mult_assoc";
 
-qed_goal "preal_mult_left_commute" thy
-    "(z1::preal) * (z2 * z3) = z2 * (z1 * z3)"
- (fn _ => [rtac (preal_mult_commute RS trans) 1, 
-           rtac (preal_mult_assoc RS trans) 1,
-           rtac (preal_mult_commute RS arg_cong) 1]);
+Goal "(z1::preal) * (z2 * z3) = z2 * (z1 * z3)";
+by (rtac (preal_mult_commute RS trans) 1);
+by (rtac (preal_mult_assoc RS trans) 1);
+by (rtac (preal_mult_commute RS arg_cong) 1);
+qed "preal_mult_left_commute";
 
 (* Positive Reals multiplication is an AC operator *)
 bind_thms ("preal_mult_ac", [preal_mult_assoc, 
@@ -397,12 +398,13 @@
 
 (** Lemmas **)
 
-qed_goal "preal_add_assoc_cong" thy
-    "!!z. (z::preal) + v = z' + v' ==> z + (v + w) = z' + (v' + w)"
- (fn _ => [(asm_simp_tac (simpset() addsimps [preal_add_assoc RS sym]) 1)]);
+Goal "(z::preal) + v = z' + v' ==> z + (v + w) = z' + (v' + w)";
+by (asm_simp_tac (simpset() addsimps [preal_add_assoc RS sym]) 1);
+qed "preal_add_assoc_cong";
 
-qed_goal "preal_add_assoc_swap" thy "(z::preal) + (v + w) = v + (z + w)"
- (fn _ => [(REPEAT (ares_tac [preal_add_commute RS preal_add_assoc_cong] 1))]);
+Goal "(z::preal) + (v + w) = v + (z + w)";
+by (REPEAT (ares_tac [preal_add_commute RS preal_add_assoc_cong] 1));
+qed "preal_add_assoc_swap";
 
 (** Distribution of multiplication across addition **)
 (** lemmas for the proof **)

--- a/src/HOL/Real/RealDef.ML	Thu Jul 06 13:35:40 2000 +0200
+++ b/src/HOL/Real/RealDef.ML	Thu Jul 06 15:01:52 2000 +0200
@@ -434,12 +434,13 @@
 
 (** Lemmas **)
 
-qed_goal "real_add_assoc_cong" thy
-    "!!z. (z::real) + v = z' + v' ==> z + (v + w) = z' + (v' + w)"
- (fn _ => [(asm_simp_tac (simpset() addsimps [real_add_assoc RS sym]) 1)]);
+Goal "(z::real) + v = z' + v' ==> z + (v + w) = z' + (v' + w)";
+by (asm_simp_tac (simpset() addsimps [real_add_assoc RS sym]) 1);
+qed "real_add_assoc_cong";
 
-qed_goal "real_add_assoc_swap" thy "(z::real) + (v + w) = v + (z + w)"
- (fn _ => [(REPEAT (ares_tac [real_add_commute RS real_add_assoc_cong] 1))]);
+Goal "(z::real) + (v + w) = v + (z + w)";
+by (REPEAT (ares_tac [real_add_commute RS real_add_assoc_cong] 1));
+qed "real_add_assoc_swap";
 
 Goal "((z1::real) + z2) * w = (z1 * w) + (z2 * w)";
 by (res_inst_tac [("z","z1")] eq_Abs_real 1);