--- 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)";
--- 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";
--- 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*)
--- 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";
--- 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";
--- 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)";
--- 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)";
--- 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}";
--- 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.";