# HG changeset patch
# User paulson
# Date 907749067 -7200
# Node ID 721671c68324bb3091bc4a687c6b50e2133aac5c
# Parent  fc3a8b82d7c28e3070ec1ab27bb3d2703cdfff7d
tidied

diff -r fc3a8b82d7c2 -r 721671c68324 src/HOL/Induct/Acc.ML
--- a/src/HOL/Induct/Acc.ML	Wed Oct 07 10:30:47 1998 +0200
+++ b/src/HOL/Induct/Acc.ML	Wed Oct 07 10:31:07 1998 +0200
@@ -12,8 +12,8 @@
 (*The intended introduction rule*)
 val prems = goal Acc.thy
     "[| !!b. (b,a):r ==> b: acc(r) |] ==> a: acc(r)";
-by (fast_tac (claset() addIs (prems @ 
-                            map (rewrite_rule [pred_def]) acc.intrs)) 1);
+by (fast_tac (claset() addIs prems @ 
+                             map (rewrite_rule [pred_def]) acc.intrs) 1);
 qed "accI";
 
 Goal "[| b: acc(r);  (a,b): r |] ==> a: acc(r)";
diff -r fc3a8b82d7c2 -r 721671c68324 src/HOL/Induct/LFilter.ML
--- a/src/HOL/Induct/LFilter.ML	Wed Oct 07 10:30:47 1998 +0200
+++ b/src/HOL/Induct/LFilter.ML	Wed Oct 07 10:31:07 1998 +0200
@@ -58,7 +58,7 @@
     "[| !!x. p x ==> q x |] ==> Domain (findRel p) <= Domain (findRel q)";
 by (Clarify_tac 1);
 by (etac findRel.induct 1);
-by (blast_tac (claset() addIs (findRel.intrs@prems)) 1);
+by (blast_tac (claset() addIs findRel.intrs @ prems) 1);
 by (blast_tac (claset() addIs findRel.intrs) 1);
 qed "Domain_findRel_mono";
 
diff -r fc3a8b82d7c2 -r 721671c68324 src/HOL/Induct/Simult.ML
--- a/src/HOL/Induct/Simult.ML	Wed Oct 07 10:30:47 1998 +0200
+++ b/src/HOL/Induct/Simult.ML	Wed Oct 07 10:31:07 1998 +0200
@@ -28,7 +28,7 @@
 Goalw [TF_def] "TF(sexp) <= sexp";
 by (rtac lfp_lowerbound 1);
 by (blast_tac (claset() addIs  sexp.intrs@[sexp_In0I, sexp_In1I]
-                      addSEs [PartE]) 1);
+                        addSEs [PartE]) 1);
 qed "TF_sexp";
 
 (* A <= sexp ==> TF(A) <= sexp *)
@@ -48,8 +48,7 @@
 \            |] ==> R(FCONS M N)    \
 \    |] ==> R(i)";
 by (rtac ([TF_def, TF_fun_mono, major] MRS def_induct) 1);
-by (blast_tac (claset() addIs (prems@[PartI])
-                       addEs [usumE, uprodE, PartE]) 1);
+by (blast_tac (claset() addIs prems@[PartI] addEs [usumE, uprodE, PartE]) 1);
 qed "TF_induct";
 
 (*This lemma replaces a use of subgoal_tac to prove tree_forest_induct*)
diff -r fc3a8b82d7c2 -r 721671c68324 src/HOL/ex/Puzzle.ML
--- a/src/HOL/ex/Puzzle.ML	Wed Oct 07 10:30:47 1998 +0200
+++ b/src/HOL/ex/Puzzle.ML	Wed Oct 07 10:31:07 1998 +0200
@@ -51,7 +51,7 @@
 qed "mono_lemma";
 
 val prems = goal Puzzle.thy "m <= n ==> f(m) <= f(n)";
-by (fast_tac (claset() addIs ([mono_lemma,less_imp_le,lemma2]@prems)) 1);
+by (fast_tac (claset() addIs [mono_lemma,less_imp_le,lemma2]@prems) 1);
 qed "f_mono";
 
 Goal "f(n) = n";
diff -r fc3a8b82d7c2 -r 721671c68324 src/HOLCF/IMP/Denotational.ML
--- a/src/HOLCF/IMP/Denotational.ML	Wed Oct 07 10:30:47 1998 +0200
+++ b/src/HOLCF/IMP/Denotational.ML	Wed Oct 07 10:31:07 1998 +0200
@@ -30,22 +30,22 @@
 
 Goal "!s t. D c`(Discr s) = (Def t) --> <c,s> -c-> t";
 by (induct_tac "c" 1);
-    by (fast_tac ((HOL_cs addSIs evalc.intrs) addss simpset()) 1);
+    by (Force_tac 1);
    by (Force_tac 1);
   by (Force_tac 1);
  by (Simp_tac 1);
- by (fast_tac ((HOL_cs addIs evalc.intrs) addss simpset()) 1);
+ by (Force_tac 1);
 by (Simp_tac 1);
 by (rtac fix_ind 1);
-  by (fast_tac (HOL_cs addSIs (adm_lemmas@[adm_chfindom,ax_flat_lift])) 1);
+  by (fast_tac (claset() addSIs adm_lemmas@[adm_chfindom,ax_flat_lift]) 1);
  by (Simp_tac 1);
 by (Simp_tac 1);
-by (safe_tac HOL_cs);
-  by (fast_tac (HOL_cs addIs evalc.intrs) 1);
- by (fast_tac ((HOL_cs addSIs evalc.intrs) addss simpset()) 1);
+by Safe_tac;
+  by (Fast_tac 1);
+ by (Force_tac 1);
 qed_spec_mp "D_implies_eval";
 
 
 Goal "(D c`(Discr s) = (Def t)) = (<c,s> -c-> t)";
-by (fast_tac (HOL_cs addSEs [D_implies_eval,eval_implies_D]) 1);
+by (fast_tac (claset() addSEs [D_implies_eval,eval_implies_D]) 1);
 qed "D_is_eval";
diff -r fc3a8b82d7c2 -r 721671c68324 src/ZF/OrderType.ML
--- a/src/ZF/OrderType.ML	Wed Oct 07 10:30:47 1998 +0200
+++ b/src/ZF/OrderType.ML	Wed Oct 07 10:31:07 1998 +0200
@@ -510,9 +510,9 @@
 val prems = 
 Goal "[| Ord(i);  !!x. x:A ==> Ord(j(x));  a:A |] ==> \
 \     i ++ (UN x:A. j(x)) = (UN x:A. i++j(x))";
-by (blast_tac (claset() addIs (prems @ [ltI, Ord_UN, Ord_oadd, 
-                                    lt_oadd1 RS ltD, oadd_lt_mono2 RS ltD])
-                     addSEs [ltE, ltI RS lt_oadd_disj RS disjE]) 1);
+by (blast_tac (claset() addIs prems @ [ltI, Ord_UN, Ord_oadd, 
+				       lt_oadd1 RS ltD, oadd_lt_mono2 RS ltD]
+                        addSEs [ltE, ltI RS lt_oadd_disj RS disjE]) 1);
 qed "oadd_UN";
 
 Goal "[| Ord(i);  Limit(j) |] ==> i++j = (UN k:j. i++k)";
diff -r fc3a8b82d7c2 -r 721671c68324 src/ZF/ex/Acc.ML
--- a/src/ZF/ex/Acc.ML	Wed Oct 07 10:30:47 1998 +0200
+++ b/src/ZF/ex/Acc.ML	Wed Oct 07 10:31:07 1998 +0200
@@ -17,7 +17,7 @@
 (*The intended introduction rule*)
 val prems = goal Acc.thy
     "[| !!b. <b,a>:r ==> b: acc(r);  a: field(r) |] ==> a: acc(r)";
-by (fast_tac (claset() addIs (prems@acc.intrs)) 1);
+by (fast_tac (claset() addIs prems@acc.intrs) 1);
 qed "accI";
 
 Goal "[| b: acc(r);  <a,b>: r |] ==> a: acc(r)";
diff -r fc3a8b82d7c2 -r 721671c68324 src/ZF/ex/ListN.ML
--- a/src/ZF/ex/ListN.ML	Wed Oct 07 10:30:47 1998 +0200
+++ b/src/ZF/ex/ListN.ML	Wed Oct 07 10:31:07 1998 +0200
@@ -20,8 +20,8 @@
 Goal "<n,l> : listn(A) <-> l:list(A) & length(l)=n";
 by (rtac iffI 1);
 by (etac listn.induct 1);
-by (safe_tac (claset() addSIs (list_typechecks @
-                            [length_Nil, length_Cons, list_into_listn])));
+by (safe_tac (claset() addSIs list_typechecks @
+                              [length_Nil, length_Cons, list_into_listn]));
 qed "listn_iff";
 
 Goal "listn(A)``{n} = {l:list(A). length(l)=n}";
diff -r fc3a8b82d7c2 -r 721671c68324 src/ZF/ex/PropLog.ML
--- a/src/ZF/ex/PropLog.ML	Wed Oct 07 10:30:47 1998 +0200
+++ b/src/ZF/ex/PropLog.ML	Wed Oct 07 10:31:07 1998 +0200
@@ -17,21 +17,18 @@
 
 Goal "prop_rec(Fls,b,c,d) = b";
 by (rtac (prop_rec_def RS def_Vrec RS trans) 1);
-by (rewrite_goals_tac prop.con_defs);
-by (Simp_tac 1);
+by (simp_tac (simpset() addsimps prop.con_defs) 1);
 qed "prop_rec_Fls";
 
 Goal "prop_rec(#v,b,c,d) = c(v)";
 by (rtac (prop_rec_def RS def_Vrec RS trans) 1);
-by (rewrite_goals_tac prop.con_defs);
-by (Simp_tac 1);
+by (simp_tac (simpset() addsimps prop.con_defs) 1);
 qed "prop_rec_Var";
 
 Goal "prop_rec(p=>q,b,c,d) = \
 \      d(p, q, prop_rec(p,b,c,d), prop_rec(q,b,c,d))";
 by (rtac (prop_rec_def RS def_Vrec RS trans) 1);
-by (rewrite_goals_tac prop.con_defs);
-by (simp_tac rank_ss 1);
+by (simp_tac (rank_ss addsimps prop.con_defs) 1);
 qed "prop_rec_Imp";
 
 Addsimps [prop_rec_Fls, prop_rec_Var, prop_rec_Imp];
@@ -41,17 +38,15 @@
 (** The function is_true **)
 
 Goalw [is_true_def] "is_true(Fls,t) <-> False";
-by (simp_tac (simpset() addsimps [one_not_0 RS not_sym]) 1);
+by (Simp_tac 1);
 qed "is_true_Fls";
 
 Goalw [is_true_def] "is_true(#v,t) <-> v:t";
-by (simp_tac (simpset() addsimps [one_not_0 RS not_sym] 
-              setloop (split_tac [split_if])) 1);
+by (Simp_tac 1);
 qed "is_true_Var";
 
-Goalw [is_true_def]
-    "is_true(p=>q,t) <-> (is_true(p,t)-->is_true(q,t))";
-by (simp_tac (simpset() setloop (split_tac [split_if])) 1);
+Goalw [is_true_def] "is_true(p=>q,t) <-> (is_true(p,t)-->is_true(q,t))";
+by (Simp_tac 1);
 qed "is_true_Imp";
 
 (** The function hyps **)
@@ -176,7 +171,7 @@
 by (safe_tac (claset() addSEs [Fls_Imp RS weaken_left_Un1, 
 			       Fls_Imp RS weaken_left_Un2]));
 by (ALLGOALS (fast_tac (claset() addIs [weaken_left_Un1, weaken_left_Un2, 
-                                     weaken_right, Imp_Fls])));
+					weaken_right, Imp_Fls])));
 qed "hyps_thms_if";
 
 (*Key lemma for completeness; yields a set of assumptions satisfying p*)
@@ -210,7 +205,7 @@
 Goal "p: prop ==> hyps(p, t-{v}) <= cons(#v=>Fls, hyps(p,t)-{#v})";
 by (etac prop.induct 1);
 by (Simp_tac 1);
-by (asm_simp_tac (simpset() setloop (split_tac [split_if])) 1);
+by (Asm_simp_tac 1);
 by (fast_tac (claset() addSEs prop.free_SEs) 1);
 by (Asm_simp_tac 1);
 by (Fast_tac 1);
@@ -221,7 +216,7 @@
 Goal "p: prop ==> hyps(p, cons(v,t)) <= cons(#v, hyps(p,t)-{#v=>Fls})";
 by (etac prop.induct 1);
 by (Simp_tac 1);
-by (asm_simp_tac (simpset() setloop (split_tac [split_if])) 1);
+by (Asm_simp_tac 1);
 by (fast_tac (claset() addSEs prop.free_SEs) 1);
 by (Asm_simp_tac 1);
 by (Fast_tac 1);
@@ -241,8 +236,7 @@
  could probably prove the stronger hyps(p,t) : Fin(hyps(p,0) Un hyps(p,nat))*)
 Goal "p: prop ==> hyps(p,t) : Fin(UN v:nat. {#v, #v=>Fls})";
 by (etac prop.induct 1);
-by (asm_simp_tac (simpset() addsimps [UN_I]
-                  setloop (split_tac [split_if])) 2);
+by (asm_simp_tac (simpset() addsimps [UN_I]) 2);
 by (ALLGOALS Asm_simp_tac);
 by (fast_tac (claset() addIs Fin.intrs) 1);
 qed "hyps_finite";
@@ -298,7 +292,7 @@
 
 val [finite] = goal PropLog.thy "H: Fin(prop) ==> H |- p <-> H |= p & p:prop";
 by (fast_tac (claset() addSEs [soundness, finite RS completeness, 
-                            thms_in_pl]) 1);
+			       thms_in_pl]) 1);
 qed "thms_iff";
 
 writeln"Reached end of file.";