expandshort and tidying

--- a/src/HOL/Fun.ML	Tue Jul 27 10:30:26 1999 +0200
+++ b/src/HOL/Fun.ML	Tue Jul 27 17:19:31 1999 +0200
@@ -7,7 +7,7 @@
 *)
 
 
-Goal "(f = g) = (!x. f(x)=g(x))";
+Goal "(f = g) = (! x. f(x)=g(x))";
 by (rtac iffI 1);
 by (Asm_simp_tac 1);
 by (rtac ext 1 THEN Asm_simp_tac 1);
@@ -33,25 +33,34 @@
 
 section "id";
 
-qed_goalw "id_apply" thy [id_def] "id x = x" (K [rtac refl 1]);
+Goalw [id_def] "id x = x";
+by (rtac refl 1);
+qed "id_apply";
 Addsimps [id_apply];
 
 
 section "o";
 
-qed_goalw "o_apply" thy [o_def] "(f o g) x = f (g x)"
- (K [rtac refl 1]);
+Goalw [o_def] "(f o g) x = f (g x)";
+by (rtac refl 1);
+qed "o_apply";
 Addsimps [o_apply];
 
-qed_goalw "o_assoc" thy [o_def] "f o (g o h) = f o g o h"
-  (K [rtac ext 1, rtac refl 1]);
+Goalw [o_def] "f o (g o h) = f o g o h";
+by (rtac ext 1);
+by (rtac refl 1);
+qed "o_assoc";
 
-qed_goalw "id_o" thy [id_def] "id o g = g"
- (K [rtac ext 1, Simp_tac 1]);
+Goalw [id_def] "id o g = g";
+by (rtac ext 1);
+by (Simp_tac 1);
+qed "id_o";
 Addsimps [id_o];
 
-qed_goalw "o_id" thy [id_def] "f o id = f"
- (K [rtac ext 1, Simp_tac 1]);
+Goalw [id_def] "f o id = f";
+by (rtac ext 1);
+by (Simp_tac 1);
+qed "o_id";
 Addsimps [o_id];
 
 Goalw [o_def] "(f o g)``r = f``(g``r)";
@@ -66,12 +75,12 @@
 (** datatypes involving function types                            **)
 
 Goalw [o_def]
-  "[| !x y. g (f x) = g y --> f x = y; g o f = g o fa |] ==> f = fa";
-br ext 1;
-be allE 1;
-be allE 1;
-be mp 1;
-be fun_cong 1;
+  "[| ! x y. g (f x) = g y --> f x = y; g o f = g o fa |] ==> f = fa";
+by (rtac ext 1);
+by (etac allE 1);
+by (etac allE 1);
+by (etac mp 1);
+by (etac fun_cong 1);
 qed "inj_fun_lemma";
 
 
@@ -272,15 +281,20 @@
 qed "fun_upd_apply";
 Addsimps [fun_upd_apply];
 
-qed_goal "fun_upd_same" thy "(f(x:=y)) x = y" 
-	(K [Simp_tac 1]);
-qed_goal "fun_upd_other" thy "!!X. z~=x ==> (f(x:=y)) z = f z"
-	(K [Asm_simp_tac 1]);
-(*Addsimps [fun_upd_same, fun_upd_other];*)
+Goal "(f(x:=y)) x = y";
+by (Simp_tac 1);
+qed "fun_upd_same";
+
+Goal "z~=x ==> (f(x:=y)) z = f z";
+by (Asm_simp_tac 1);
+qed "fun_upd_other";
+
+(*Currently unused?
+  We could try Addsimps [fun_upd_same, fun_upd_other];*)
 
 Goal "a ~= c ==> m(a:=b)(c:=d) = m(c:=d)(a:=b)";
 by (rtac ext 1);
-by (Auto_tac);
+by Auto_tac;
 qed "fun_upd_twist";
 
 

--- a/src/HOL/Nat.ML	Tue Jul 27 10:30:26 1999 +0200
+++ b/src/HOL/Nat.ML	Tue Jul 27 17:19:31 1999 +0200
@@ -33,14 +33,13 @@
 
 Goal "(n ~= 0) = (0 < n)";
 by (exhaust_tac "n" 1);
-by (Blast_tac 1);
-by (Blast_tac 1);
+by Auto_tac;
 qed "neq0_conv";
 AddIffs [neq0_conv];
 
 Goal "(0 ~= n) = (0 < n)";
 by (exhaust_tac "n" 1);
-by (Auto_tac);
+by Auto_tac;
 qed "zero_neq_conv";
 AddIffs [zero_neq_conv];
 
@@ -75,33 +74,16 @@
 by (hyp_subst_tac 1);
 by (rewtac Least_nat_def);
 by (rtac (select_equality RS arg_cong RS sym) 1);
-by (Safe_tac);
-by (dtac Suc_mono 1);
-by (Blast_tac 1);
-by (cut_facts_tac [less_linear] 1);
-by (Safe_tac);
-by (atac 2);
-by (Blast_tac 2);
-by (dtac Suc_mono 1);
-by (Blast_tac 1);
+by (blast_tac (claset() addDs [Suc_mono]) 1);
+by (cut_inst_tac [("m","m")] less_linear 1);
+by (blast_tac (claset() addIs [Suc_mono]) 1);
 qed "Least_Suc";
 
 val prems = Goal "[| P 0; P 1; !!k. P k ==> P (Suc (Suc k)) |] ==> P n";
-by (cut_facts_tac prems 1);
 by (rtac less_induct 1);
 by (exhaust_tac "n" 1);
-by (hyp_subst_tac 1);
-by (atac 1);
-by (hyp_subst_tac 1);
-by (exhaust_tac "nat" 1);
-by (hyp_subst_tac 1);
-by (atac 1);
-by (hyp_subst_tac 1);
-by (resolve_tac prems 1);
-by (dtac spec 1);
-by (etac mp 1);
-by (rtac (lessI RS less_trans) 1);
-by (rtac (lessI RS Suc_mono) 1);
+by (exhaust_tac "nat" 2);
+by (ALLGOALS (blast_tac (claset() addIs prems@[less_trans])));
 qed "nat_induct2";
 
 Goal "min 0 n = 0";