# HG changeset patch
# User paulson
# Date 878734259 -3600
# Node ID 4c2da701b801e281fdfa55232908dc58228dd3ef
# Parent  ac7f082e64a58711846cb54a0f313dc13ebc53d7
Ran expandshort, especially to introduce Safe_tac

diff -r ac7f082e64a5 -r 4c2da701b801 src/HOL/Integ/Integ.ML
--- a/src/HOL/Integ/Integ.ML	Wed Nov 05 13:50:16 1997 +0100
+++ b/src/HOL/Integ/Integ.ML	Wed Nov 05 13:50:59 1997 +0100
@@ -105,7 +105,7 @@
 by (dtac eq_equiv_class 1);
 by (rtac equiv_intrel 1);
 by (Fast_tac 1);
-by (safe_tac (claset()));
+by Safe_tac;
 by (Asm_full_simp_tac 1);
 qed "inj_znat";
 
@@ -114,7 +114,7 @@
 
 goalw Integ.thy [congruent_def]
   "congruent intrel (%p. split (%x y. intrel^^{(y,x)}) p)";
-by (safe_tac (claset()));
+by Safe_tac;
 by (asm_simp_tac (simpset() addsimps add_ac) 1);
 qed "zminus_congruent";
 
@@ -169,7 +169,7 @@
 goalw Integ.thy [znegative_def, znat_def]
     "~ znegative($# n)";
 by (Simp_tac 1);
-by (safe_tac (claset()));
+by Safe_tac;
 by (rtac ccontr 1);
 by (etac notE 1);
 by (Asm_full_simp_tac 1);
@@ -201,7 +201,7 @@
 
 goalw Integ.thy [congruent_def]
     "congruent intrel (split (%x y. intrel^^{((y-x) + (x-(y::nat)),0)}))";
-by (safe_tac (claset()));
+by Safe_tac;
 by (Asm_simp_tac 1);
 by (etac rev_mp 1);
 by (res_inst_tac [("m","x1"),("n","y1")] diff_induct 1);
@@ -246,7 +246,7 @@
     "congruent2 intrel (%p1 p2.                  \
 \         split (%x1 y1. split (%x2 y2. intrel^^{(x1+x2, y1+y2)}) p2) p1)";
 (*Proof via congruent2_commuteI seems longer*)
-by (safe_tac (claset()));
+by Safe_tac;
 by (asm_simp_tac (simpset() addsimps [add_assoc]) 1);
 (*The rest should be trivial, but rearranging terms is hard*)
 by (res_inst_tac [("x1","x1a")] (add_left_commute RS ssubst) 1);
@@ -343,7 +343,7 @@
 \               split (%x1 y1. split (%x2 y2.   \
 \                   intrel^^{(x1*x2 + y1*y2, x1*y2 + y1*x2)}) p2) p1)";
 by (rtac (equiv_intrel RS congruent2_commuteI) 1);
-by (safe_tac (claset()));
+by Safe_tac;
 by (rewtac split_def);
 by (simp_tac (simpset() addsimps add_ac@mult_ac) 1);
 by (asm_simp_tac (simpset() delsimps [equiv_intrel_iff]
@@ -477,31 +477,31 @@
 qed "zsuc_zpred";
 
 goal Integ.thy "(zpred(z)=w) = (z=zsuc(w))";
-by (safe_tac (claset()));
+by Safe_tac;
 by (rtac (zsuc_zpred RS sym) 1);
 by (rtac zpred_zsuc 1);
 qed "zpred_to_zsuc";
 
 goal Integ.thy "(zsuc(z)=w)=(z=zpred(w))";
-by (safe_tac (claset()));
+by Safe_tac;
 by (rtac (zpred_zsuc RS sym) 1);
 by (rtac zsuc_zpred 1);
 qed "zsuc_to_zpred";
 
 goal Integ.thy "($~ z = w) = (z = $~ w)";
-by (safe_tac (claset()));
+by Safe_tac;
 by (rtac (zminus_zminus RS sym) 1);
 by (rtac zminus_zminus 1);
 qed "zminus_exchange";
 
 goal Integ.thy"(zsuc(z)=zsuc(w)) = (z=w)";
-by (safe_tac (claset()));
+by Safe_tac;
 by (dres_inst_tac [("f","zpred")] arg_cong 1);
 by (asm_full_simp_tac (simpset() addsimps [zpred_zsuc]) 1);
 qed "bijective_zsuc";
 
 goal Integ.thy"(zpred(z)=zpred(w)) = (z=w)";
-by (safe_tac (claset()));
+by Safe_tac;
 by (dres_inst_tac [("f","zsuc")] arg_cong 1);
 by (asm_full_simp_tac (simpset() addsimps [zsuc_zpred]) 1);
 qed "bijective_zpred";
@@ -560,7 +560,7 @@
 val zsuc_n_not_n = n_not_zsuc_n RS not_sym;
 
 goal Integ.thy "w ~= zpred(w)";
-by (safe_tac (claset()));
+by Safe_tac;
 by (dres_inst_tac [("x","w"),("f","zsuc")] arg_cong 1);
 by (asm_full_simp_tac (simpset() addsimps [zsuc_zpred,zsuc_n_not_n]) 1);
 qed "n_not_zpred_n";
@@ -574,7 +574,7 @@
     "!!w. w<z ==> ? n. z = w + $#(Suc(n))";
 by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
 by (res_inst_tac [("z","w")] eq_Abs_Integ 1);
-by (safe_tac (claset()));
+by Safe_tac;
 by (asm_full_simp_tac (simpset() addsimps [zadd, zminus]) 1);
 by (safe_tac (claset() addSDs [less_eq_Suc_add]));
 by (rename_tac "k" 1);
@@ -589,7 +589,7 @@
 goalw Integ.thy [zless_def, znegative_def, zdiff_def, znat_def] 
     "z < z + $#(Suc(n))";
 by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
-by (safe_tac (claset()));
+by Safe_tac;
 by (simp_tac (simpset() addsimps [zadd, zminus]) 1);
 by (REPEAT_SOME (ares_tac [refl, exI, singletonI, ImageI, conjI, intrelI]));
 by (rtac le_less_trans 1);
@@ -612,7 +612,7 @@
 goal Integ.thy "!!z w::int. z<w ==> ~w<z";
 by (safe_tac (claset() addSDs [zless_eq_zadd_Suc]));
 by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
-by (safe_tac (claset()));
+by Safe_tac;
 by (asm_full_simp_tac (simpset() addsimps ([znat_def, zadd])) 1);
 by (asm_full_simp_tac
  (simpset() delsimps [add_Suc_right] addsimps [add_left_cancel, add_assoc, add_Suc_right RS sym]) 1);
@@ -642,7 +642,7 @@
     "z<w | z=w | w<(z::int)";
 by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
 by (res_inst_tac [("z","w")] eq_Abs_Integ 1);
-by (safe_tac (claset()));
+by Safe_tac;
 by (asm_full_simp_tac
     (simpset() addsimps [zadd, zminus, Image_iff, Bex_def]) 1);
 by (res_inst_tac [("m1", "x+ya"), ("n1", "xa+y")] (less_linear RS disjE) 1);
diff -r ac7f082e64a5 -r 4c2da701b801 src/HOL/Lambda/Eta.ML
--- a/src/HOL/Lambda/Eta.ML	Wed Nov 05 13:50:16 1997 +0100
+++ b/src/HOL/Lambda/Eta.ML	Wed Nov 05 13:50:59 1997 +0100
@@ -37,7 +37,7 @@
 by (dB.induct_tac "t" 1);
 by (ALLGOALS(asm_full_simp_tac (addsplit (simpset()) addcongs [conj_cong])));
 by (Blast_tac 2);
-by(simp_tac (simpset() addsimps [pred_def] addsplits [expand_nat_case]) 1);
+by (simp_tac (simpset() addsimps [pred_def] addsplits [expand_nat_case]) 1);
 by (safe_tac HOL_cs);
 by (ALLGOALS trans_tac);
 qed "free_lift";
@@ -49,7 +49,7 @@
 by (Asm_simp_tac 2);
 by (Blast_tac 2);
 by (asm_full_simp_tac (addsplit (simpset())) 2);
-by(simp_tac (simpset() addsimps [pred_def,subst_Var]
+by (simp_tac (simpset() addsimps [pred_def,subst_Var]
                       addsplits [expand_if,expand_nat_case]) 1);
 by (safe_tac (HOL_cs addSEs [nat_neqE]));
 by (ALLGOALS trans_tac);
@@ -79,7 +79,7 @@
 by (etac eta.induct 1);
 by (slow_tac (claset() addIs [subst_not_free,eta_subst]
                       addIs [free_eta RS iffD1] addss simpset()) 1);
-by (safe_tac (claset()));
+by Safe_tac;
 by (blast_tac (claset() addSIs [eta_subst] addIs [free_eta RS iffD1]) 5);
 by (ALLGOALS Blast_tac);
 qed "square_eta";
@@ -126,8 +126,8 @@
 goal Eta.thy "!i. t[Var i/i] = t[Var(i)/Suc i]";
 by (dB.induct_tac "t" 1);
 by (ALLGOALS (asm_simp_tac (addsplit (simpset()))));
-by(safe_tac (HOL_cs addSEs [nat_neqE]));
-by(ALLGOALS trans_tac);
+by (safe_tac (HOL_cs addSEs [nat_neqE]));
+by (ALLGOALS trans_tac);
 qed_spec_mp "subst_Var_Suc";
 Addsimps [subst_Var_Suc];
 
@@ -170,7 +170,7 @@
 by (dB.induct_tac "s" 1);
   by (simp_tac (simpset() addsplits [expand_if]) 1);
   by (SELECT_GOAL(safe_tac HOL_cs)1);
-   by(etac nat_neqE 1);
+   by (etac nat_neqE 1);
     by (res_inst_tac [("x","Var nat")] exI 1);
     by (Asm_simp_tac 1);
    by (res_inst_tac [("x","Var(pred nat)")] exI 1);
diff -r ac7f082e64a5 -r 4c2da701b801 src/HOL/Lex/Auto.ML
--- a/src/HOL/Lex/Auto.ML	Wed Nov 05 13:50:16 1997 +0100
+++ b/src/HOL/Lex/Auto.ML	Wed Nov 05 13:50:59 1997 +0100
@@ -7,32 +7,32 @@
 open Auto;
 
 goalw Auto.thy [nexts_def] "nexts A st [] = st";
-by(Simp_tac 1);
+by (Simp_tac 1);
 qed"nexts_Nil";
 
 goalw Auto.thy [nexts_def] "nexts A st (x#xs) = nexts A (next A st x) xs";
-by(Simp_tac 1);
+by (Simp_tac 1);
 qed"nexts_Cons";
 
 Addsimps [nexts_Nil,nexts_Cons];
 
 goalw Auto.thy [acc_prefix_def] "~acc_prefix A st []";
-by(Simp_tac 1);
+by (Simp_tac 1);
 qed"acc_prefix_Nil";
 Addsimps [acc_prefix_Nil];
 
 goalw Auto.thy [acc_prefix_def]
  "acc_prefix A s (x#xs) = (fin A (next A s x) | acc_prefix A (next A s x) xs)";
-by(simp_tac (simpset() addsimps [prefix_Cons]) 1);
-by(safe_tac (claset()));
-  by(Asm_full_simp_tac 1);
+by (simp_tac (simpset() addsimps [prefix_Cons]) 1);
+by Safe_tac;
+  by (Asm_full_simp_tac 1);
   by (case_tac "zs=[]" 1);
-   by(hyp_subst_tac 1);
-   by(Asm_full_simp_tac 1);
-  by(Fast_tac 1);
- by(res_inst_tac [("x","[x]")] exI 1);
- by(asm_simp_tac (simpset() addsimps [eq_sym_conv]) 1);
-by(res_inst_tac [("x","x#us")] exI 1);
-by(Asm_simp_tac 1);
+   by (hyp_subst_tac 1);
+   by (Asm_full_simp_tac 1);
+  by (Fast_tac 1);
+ by (res_inst_tac [("x","[x]")] exI 1);
+ by (asm_simp_tac (simpset() addsimps [eq_sym_conv]) 1);
+by (res_inst_tac [("x","x#us")] exI 1);
+by (Asm_simp_tac 1);
 qed"acc_prefix_Cons";
 Addsimps [acc_prefix_Cons];