--- a/src/FOLP/IFOLP.thy Sun Nov 20 17:57:09 2011 +0100
+++ b/src/FOLP/IFOLP.thy Sun Nov 20 20:15:02 2011 +0100
@@ -504,7 +504,7 @@
lemmas pred_congs = pred1_cong pred2_cong pred3_cong
(*special case for the equality predicate!*)
-lemmas eq_cong = pred2_cong [where P = "op =", standard]
+lemmas eq_cong = pred2_cong [where P = "op ="]
(*** Simplifications of assumed implications.
--- a/src/Sequents/LK.thy Sun Nov 20 17:57:09 2011 +0100
+++ b/src/Sequents/LK.thy Sun Nov 20 20:15:02 2011 +0100
@@ -129,14 +129,14 @@
apply (tactic {* fast_tac LK_pack 1 *})
done
-lemmas iff_reflection_F = P_iff_F [THEN iff_reflection, standard]
+lemmas iff_reflection_F = P_iff_F [THEN iff_reflection]
lemma P_iff_T: "|- P ==> |- (P <-> True)"
apply (erule thinR [THEN cut])
apply (tactic {* fast_tac LK_pack 1 *})
done
-lemmas iff_reflection_T = P_iff_T [THEN iff_reflection, standard]
+lemmas iff_reflection_T = P_iff_T [THEN iff_reflection]
lemma LK_extra_simps:
--- a/src/Sequents/LK0.thy Sun Nov 20 17:57:09 2011 +0100
+++ b/src/Sequents/LK0.thy Sun Nov 20 20:15:02 2011 +0100
@@ -305,10 +305,10 @@
by (tactic {* safe_tac (LK_pack add_safes [@{thm subst}]) 1 *})
(* Symmetry of equality in hypotheses *)
-lemmas symL = sym [THEN L_of_imp, standard]
+lemmas symL = sym [THEN L_of_imp]
(* Symmetry of equality in hypotheses *)
-lemmas symR = sym [THEN R_of_imp, standard]
+lemmas symR = sym [THEN R_of_imp]
lemma transR: "[| $H|- $E, $F, a=b; $H|- $E, $F, b=c |] ==> $H|- $E, a=c, $F"
by (rule trans [THEN R_of_imp, THEN mp_R])
--- a/src/ZF/AC/HH.thy Sun Nov 20 17:57:09 2011 +0100
+++ b/src/ZF/AC/HH.thy Sun Nov 20 20:15:02 2011 +0100
@@ -210,7 +210,7 @@
simplification is needed!*)
lemmas bij_Least_HH_x =
comp_bij [OF f_sing_lam_bij [OF _ lam_singI]
- lam_sing_bij [THEN bij_converse_bij], standard]
+ lam_sing_bij [THEN bij_converse_bij]]
subsection{*The proof of AC1 ==> WO2*}
--- a/src/ZF/AC/Hartog.thy Sun Nov 20 17:57:09 2011 +0100
+++ b/src/ZF/AC/Hartog.thy Sun Nov 20 20:15:02 2011 +0100
@@ -65,7 +65,7 @@
apply (rule LeastI, auto)
done
-lemmas Hartog_lepoll_selfE = not_Hartog_lepoll_self [THEN notE, standard]
+lemmas Hartog_lepoll_selfE = not_Hartog_lepoll_self [THEN notE]
lemma Ord_Hartog: "Ord(Hartog(A))"
by (unfold Hartog_def, rule Ord_Least)
--- a/src/ZF/AC/WO2_AC16.thy Sun Nov 20 17:57:09 2011 +0100
+++ b/src/ZF/AC/WO2_AC16.thy Sun Nov 20 20:15:02 2011 +0100
@@ -315,8 +315,7 @@
lemmas disj_Un_eqpoll_nat_sum =
eqpoll_trans [THEN eqpoll_trans,
- OF disj_Un_eqpoll_sum sum_eqpoll_cong nat_sum_eqpoll_sum,
- standard];
+ OF disj_Un_eqpoll_sum sum_eqpoll_cong nat_sum_eqpoll_sum];
lemma Un_in_Collect: "[| x \<in> Pow(A - B - h`i); x\<approx>m;
--- a/src/ZF/AC/WO6_WO1.thy Sun Nov 20 17:57:09 2011 +0100
+++ b/src/ZF/AC/WO6_WO1.thy Sun Nov 20 20:15:02 2011 +0100
@@ -217,10 +217,9 @@
apply (fast elim!: LeastI)+
done
-lemmas nested_Least_instance =
+lemmas nested_Least_instance =
nested_LeastI [of "%g d. domain(uu(f,b,g,d)) \<noteq> 0 &
- domain(uu(f,b,g,d)) \<lesssim> m",
- standard] (*generalizes the Variables!*)
+ domain(uu(f,b,g,d)) \<lesssim> m"] for f b m
lemma gg1_lepoll_m:
"[| Ord(a); m \<in> nat;
--- a/src/ZF/Bool.thy Sun Nov 20 17:57:09 2011 +0100
+++ b/src/ZF/Bool.thy Sun Nov 20 20:15:02 2011 +0100
@@ -53,7 +53,7 @@
by (simp add: bool_defs )
(** 1=0 ==> R **)
-lemmas one_neq_0 = one_not_0 [THEN notE, standard]
+lemmas one_neq_0 = one_not_0 [THEN notE]
lemma boolE:
"[| c: bool; c=1 ==> P; c=0 ==> P |] ==> P"
@@ -82,17 +82,17 @@
lemma def_cond_0: "[| !!b. j(b)==cond(b,c,d) |] ==> j(0) = d"
by simp
-lemmas not_1 = not_def [THEN def_cond_1, standard, simp]
-lemmas not_0 = not_def [THEN def_cond_0, standard, simp]
+lemmas not_1 = not_def [THEN def_cond_1, simp]
+lemmas not_0 = not_def [THEN def_cond_0, simp]
-lemmas and_1 = and_def [THEN def_cond_1, standard, simp]
-lemmas and_0 = and_def [THEN def_cond_0, standard, simp]
+lemmas and_1 = and_def [THEN def_cond_1, simp]
+lemmas and_0 = and_def [THEN def_cond_0, simp]
-lemmas or_1 = or_def [THEN def_cond_1, standard, simp]
-lemmas or_0 = or_def [THEN def_cond_0, standard, simp]
+lemmas or_1 = or_def [THEN def_cond_1, simp]
+lemmas or_0 = or_def [THEN def_cond_0, simp]
-lemmas xor_1 = xor_def [THEN def_cond_1, standard, simp]
-lemmas xor_0 = xor_def [THEN def_cond_0, standard, simp]
+lemmas xor_1 = xor_def [THEN def_cond_1, simp]
+lemmas xor_0 = xor_def [THEN def_cond_0, simp]
lemma not_type [TC]: "a:bool ==> not(a) : bool"
by (simp add: not_def)
--- a/src/ZF/Cardinal.thy Sun Nov 20 17:57:09 2011 +0100
+++ b/src/ZF/Cardinal.thy Sun Nov 20 20:15:02 2011 +0100
@@ -94,7 +94,7 @@
done
(*A eqpoll A*)
-lemmas eqpoll_refl = id_bij [THEN bij_imp_eqpoll, standard, simp]
+lemmas eqpoll_refl = id_bij [THEN bij_imp_eqpoll, simp]
lemma eqpoll_sym: "X \<approx> Y ==> Y \<approx> X"
apply (unfold eqpoll_def)
@@ -115,9 +115,9 @@
apply (erule id_subset_inj)
done
-lemmas lepoll_refl = subset_refl [THEN subset_imp_lepoll, standard, simp]
+lemmas lepoll_refl = subset_refl [THEN subset_imp_lepoll, simp]
-lemmas le_imp_lepoll = le_imp_subset [THEN subset_imp_lepoll, standard]
+lemmas le_imp_lepoll = le_imp_subset [THEN subset_imp_lepoll]
lemma eqpoll_imp_lepoll: "X \<approx> Y ==> X \<lesssim> Y"
by (unfold eqpoll_def bij_def lepoll_def, blast)
@@ -147,7 +147,7 @@
done
(*0 \<lesssim> Y*)
-lemmas empty_lepollI = empty_subsetI [THEN subset_imp_lepoll, standard]
+lemmas empty_lepollI = empty_subsetI [THEN subset_imp_lepoll]
lemma lepoll_0_iff: "A \<lesssim> 0 <-> A=0"
by (blast intro: lepoll_0_is_0 lepoll_refl)
@@ -159,7 +159,7 @@
done
(*A eqpoll 0 ==> A=0*)
-lemmas eqpoll_0_is_0 = eqpoll_imp_lepoll [THEN lepoll_0_is_0, standard]
+lemmas eqpoll_0_is_0 = eqpoll_imp_lepoll [THEN lepoll_0_is_0]
lemma eqpoll_0_iff: "A \<approx> 0 <-> A=0"
by (blast intro: eqpoll_0_is_0 eqpoll_refl)
@@ -791,12 +791,12 @@
[unfolded Finite_def]])
done
-lemmas subset_Finite = subset_imp_lepoll [THEN lepoll_Finite, standard]
+lemmas subset_Finite = subset_imp_lepoll [THEN lepoll_Finite]
lemma Finite_Int: "Finite(A) | Finite(B) ==> Finite(A Int B)"
by (blast intro: subset_Finite)
-lemmas Finite_Diff = Diff_subset [THEN subset_Finite, standard]
+lemmas Finite_Diff = Diff_subset [THEN subset_Finite]
lemma Finite_cons: "Finite(x) ==> Finite(cons(y,x))"
apply (unfold Finite_def)
--- a/src/ZF/CardinalArith.thy Sun Nov 20 17:57:09 2011 +0100
+++ b/src/ZF/CardinalArith.thy Sun Nov 20 20:15:02 2011 +0100
@@ -753,9 +753,9 @@
apply (blast intro: Card_jump_cardinal K_lt_jump_cardinal Ord_jump_cardinal)+
done
-lemmas Card_csucc = csucc_basic [THEN conjunct1, standard]
+lemmas Card_csucc = csucc_basic [THEN conjunct1]
-lemmas lt_csucc = csucc_basic [THEN conjunct2, standard]
+lemmas lt_csucc = csucc_basic [THEN conjunct2]
lemma Ord_0_lt_csucc: "Ord(K) ==> 0 < csucc(K)"
by (blast intro: Ord_0_le lt_csucc lt_trans1)
@@ -857,7 +857,7 @@
subsubsection{*Theorems by Krzysztof Grabczewski, proofs by lcp*}
-lemmas nat_implies_well_ord = nat_into_Ord [THEN well_ord_Memrel, standard]
+lemmas nat_implies_well_ord = nat_into_Ord [THEN well_ord_Memrel]
lemma nat_sum_eqpoll_sum: "[| m:nat; n:nat |] ==> m + n \<approx> m #+ n"
apply (rule eqpoll_trans)
--- a/src/ZF/Cardinal_AC.thy Sun Nov 20 17:57:09 2011 +0100
+++ b/src/ZF/Cardinal_AC.thy Sun Nov 20 20:15:02 2011 +0100
@@ -17,7 +17,7 @@
done
text{*The theorem @{term "||A|| = |A|"} *}
-lemmas cardinal_idem = cardinal_eqpoll [THEN cardinal_cong, standard, simp]
+lemmas cardinal_idem = cardinal_eqpoll [THEN cardinal_cong, simp]
lemma cardinal_eqE: "|X| = |Y| ==> X eqpoll Y"
apply (rule AC_well_ord [THEN exE])
--- a/src/ZF/Coind/ECR.thy Sun Nov 20 17:57:09 2011 +0100
+++ b/src/ZF/Coind/ECR.thy Sun Nov 20 20:15:02 2011 +0100
@@ -52,7 +52,7 @@
(* Properties of the pointwise extension to environments *)
lemmas HasTyRel_non_zero =
- HasTyRel.dom_subset [THEN subsetD, THEN SigmaD1, THEN ValNEE, standard]
+ HasTyRel.dom_subset [THEN subsetD, THEN SigmaD1, THEN ValNEE]
lemma hastyenv_owr:
"[| ve \<in> ValEnv; te \<in> TyEnv; hastyenv(ve,te); <v,t> \<in> HasTyRel |]
--- a/src/ZF/Constructible/Formula.thy Sun Nov 20 17:57:09 2011 +0100
+++ b/src/ZF/Constructible/Formula.thy Sun Nov 20 20:15:02 2011 +0100
@@ -805,8 +805,8 @@
apply (blast intro: doubleton_in_Lset)
done
-lemmas Lset_UnI1 = Un_upper1 [THEN Lset_mono [THEN subsetD], standard]
-lemmas Lset_UnI2 = Un_upper2 [THEN Lset_mono [THEN subsetD], standard]
+lemmas Lset_UnI1 = Un_upper1 [THEN Lset_mono [THEN subsetD]]
+lemmas Lset_UnI2 = Un_upper2 [THEN Lset_mono [THEN subsetD]]
text{*Hard work is finding a single j:i such that {a,b}<=Lset(j)*}
lemma doubleton_in_LLimit:
--- a/src/ZF/Epsilon.thy Sun Nov 20 17:57:09 2011 +0100
+++ b/src/ZF/Epsilon.thy Sun Nov 20 20:15:02 2011 +0100
@@ -45,7 +45,7 @@
apply (rule nat_0I [THEN UN_upper])
done
-lemmas arg_into_eclose = arg_subset_eclose [THEN subsetD, standard]
+lemmas arg_into_eclose = arg_subset_eclose [THEN subsetD]
lemma Transset_eclose: "Transset(eclose(A))"
apply (unfold eclose_def Transset_def)
@@ -58,13 +58,13 @@
(* x : eclose(A) ==> x <= eclose(A) *)
lemmas eclose_subset =
- Transset_eclose [unfolded Transset_def, THEN bspec, standard]
+ Transset_eclose [unfolded Transset_def, THEN bspec]
(* [| A : eclose(B); c : A |] ==> c : eclose(B) *)
-lemmas ecloseD = eclose_subset [THEN subsetD, standard]
+lemmas ecloseD = eclose_subset [THEN subsetD]
lemmas arg_in_eclose_sing = arg_subset_eclose [THEN singleton_subsetD]
-lemmas arg_into_eclose_sing = arg_in_eclose_sing [THEN ecloseD, standard]
+lemmas arg_into_eclose_sing = arg_in_eclose_sing [THEN ecloseD]
(* This is epsilon-induction for eclose(A); see also eclose_induct_down...
[| a: eclose(A); !!x. [| x: eclose(A); ALL y:x. P(y) |] ==> P(x)
@@ -148,7 +148,7 @@
by (simp add: lt_def Ord_def under_Memrel)
(* j : eclose(A) ==> Memrel(eclose(A)) -`` j = j *)
-lemmas under_Memrel_eclose = Transset_eclose [THEN under_Memrel, standard]
+lemmas under_Memrel_eclose = Transset_eclose [THEN under_Memrel]
lemmas wfrec_ssubst = wf_Memrel [THEN wfrec, THEN ssubst]
--- a/src/ZF/Finite.thy Sun Nov 20 17:57:09 2011 +0100
+++ b/src/ZF/Finite.thy Sun Nov 20 20:15:02 2011 +0100
@@ -48,7 +48,7 @@
done
(* A : Fin(B) ==> A <= B *)
-lemmas FinD = Fin.dom_subset [THEN subsetD, THEN PowD, standard]
+lemmas FinD = Fin.dom_subset [THEN subsetD, THEN PowD]
(** Induction on finite sets **)
@@ -147,7 +147,7 @@
lemma FiniteFun_domain_Fin: "h: A -||>B ==> domain(h) : Fin(A)"
by (erule FiniteFun.induct, simp, simp)
-lemmas FiniteFun_apply_type = FiniteFun_is_fun [THEN apply_type, standard]
+lemmas FiniteFun_apply_type = FiniteFun_is_fun [THEN apply_type]
(*Every subset of a finite function is a finite function.*)
lemma FiniteFun_subset_lemma [rule_format]:
--- a/src/ZF/Induct/Multiset.thy Sun Nov 20 17:57:09 2011 +0100
+++ b/src/ZF/Induct/Multiset.thy Sun Nov 20 20:15:02 2011 +0100
@@ -221,7 +221,7 @@
(** normalize **)
-lemmas Collect_Finite = Collect_subset [THEN subset_Finite, standard]
+lemmas Collect_Finite = Collect_subset [THEN subset_Finite]
lemma normalize_idem [simp]: "normalize(normalize(f)) = normalize(f)"
apply (simp add: normalize_def funrestrict_def mset_of_def)
@@ -1136,7 +1136,7 @@
subsection{*Ordinal Multisets*}
(* A \<subseteq> B ==> field(Memrel(A)) \<subseteq> field(Memrel(B)) *)
-lemmas field_Memrel_mono = Memrel_mono [THEN field_mono, standard]
+lemmas field_Memrel_mono = Memrel_mono [THEN field_mono]
(*
[| Aa \<subseteq> Ba; A \<subseteq> B |] ==>
@@ -1187,7 +1187,7 @@
part_ord(field(Memrel(i))-||>nat-{0}, multirel(field(Memrel(i)), Memrel(i)))
*)
-lemmas part_ord_mless = part_ord_Memrel [THEN part_ord_multirel, standard]
+lemmas part_ord_mless = part_ord_Memrel [THEN part_ord_multirel]
(*irreflexivity*)
@@ -1199,7 +1199,7 @@
done
(* N<N ==> R *)
-lemmas mless_irrefl = mless_not_refl [THEN notE, standard, elim!]
+lemmas mless_irrefl = mless_not_refl [THEN notE, elim!]
(*transitivity*)
lemma mless_trans: "[| K <# M; M <# N |] ==> K <# N"
--- a/src/ZF/Induct/Tree_Forest.thy Sun Nov 20 17:57:09 2011 +0100
+++ b/src/ZF/Induct/Tree_Forest.thy Sun Nov 20 20:15:02 2011 +0100
@@ -19,9 +19,10 @@
(* FIXME *)
lemmas tree'induct =
- tree_forest.mutual_induct [THEN conjunct1, THEN spec, THEN [2] rev_mp, of concl: _ t, standard, consumes 1]
+ tree_forest.mutual_induct [THEN conjunct1, THEN spec, THEN [2] rev_mp, of concl: _ t, consumes 1]
and forest'induct =
- tree_forest.mutual_induct [THEN conjunct2, THEN spec, THEN [2] rev_mp, of concl: _ f, standard, consumes 1]
+ tree_forest.mutual_induct [THEN conjunct2, THEN spec, THEN [2] rev_mp, of concl: _ f, consumes 1]
+ for t
declare tree_forest.intros [simp, TC]
--- a/src/ZF/IntArith.thy Sun Nov 20 17:57:09 2011 +0100
+++ b/src/ZF/IntArith.thy Sun Nov 20 20:15:02 2011 +0100
@@ -9,19 +9,22 @@
**)
lemmas [simp] =
- zminus_equation [where y = "integ_of(w)", standard]
- equation_zminus [where x = "integ_of(w)", standard]
+ zminus_equation [where y = "integ_of(w)"]
+ equation_zminus [where x = "integ_of(w)"]
+ for w
lemmas [iff] =
- zminus_zless [where y = "integ_of(w)", standard]
- zless_zminus [where x = "integ_of(w)", standard]
+ zminus_zless [where y = "integ_of(w)"]
+ zless_zminus [where x = "integ_of(w)"]
+ for w
lemmas [iff] =
- zminus_zle [where y = "integ_of(w)", standard]
- zle_zminus [where x = "integ_of(w)", standard]
+ zminus_zle [where y = "integ_of(w)"]
+ zle_zminus [where x = "integ_of(w)"]
+ for w
lemmas [simp] =
- Let_def [where s = "integ_of(w)", standard]
+ Let_def [where s = "integ_of(w)"] for w
(*** Simprocs for numeric literals ***)
@@ -47,12 +50,13 @@
(** For cancel_numerals **)
lemmas rel_iff_rel_0_rls =
- zless_iff_zdiff_zless_0 [where y = "u $+ v", standard]
- eq_iff_zdiff_eq_0 [where y = "u $+ v", standard]
- zle_iff_zdiff_zle_0 [where y = "u $+ v", standard]
+ zless_iff_zdiff_zless_0 [where y = "u $+ v"]
+ eq_iff_zdiff_eq_0 [where y = "u $+ v"]
+ zle_iff_zdiff_zle_0 [where y = "u $+ v"]
zless_iff_zdiff_zless_0 [where y = n]
eq_iff_zdiff_eq_0 [where y = n]
zle_iff_zdiff_zle_0 [where y = n]
+ for u v (* FIXME n (!?) *)
lemma eq_add_iff1: "(i$*u $+ m = j$*u $+ n) <-> ((i$-j)$*u $+ m = intify(n))"
apply (simp add: zdiff_def zadd_zmult_distrib)
--- a/src/ZF/IntDiv_ZF.thy Sun Nov 20 17:57:09 2011 +0100
+++ b/src/ZF/IntDiv_ZF.thy Sun Nov 20 20:15:02 2011 +0100
@@ -791,8 +791,8 @@
apply (blast dest: zle_zless_trans)+
done
-lemmas pos_mod_sign = pos_mod [THEN conjunct1, standard]
-and pos_mod_bound = pos_mod [THEN conjunct2, standard]
+lemmas pos_mod_sign = pos_mod [THEN conjunct1]
+ and pos_mod_bound = pos_mod [THEN conjunct2]
lemma neg_mod: "b $< #0 ==> a zmod b $<= #0 & b $< a zmod b"
apply (cut_tac a = "intify (a)" and b = "intify (b)" in divAlg_correct)
@@ -801,8 +801,8 @@
apply (blast dest: zless_trans)+
done
-lemmas neg_mod_sign = neg_mod [THEN conjunct1, standard]
-and neg_mod_bound = neg_mod [THEN conjunct2, standard]
+lemmas neg_mod_sign = neg_mod [THEN conjunct1]
+ and neg_mod_bound = neg_mod [THEN conjunct2]
(** proving general properties of zdiv and zmod **)
@@ -1111,16 +1111,16 @@
apply (blast dest!: zle_zless_trans)+
done
-declare zdiv_pos_pos [of "integ_of (v)" "integ_of (w)", standard, simp]
-declare zdiv_neg_pos [of "integ_of (v)" "integ_of (w)", standard, simp]
-declare zdiv_pos_neg [of "integ_of (v)" "integ_of (w)", standard, simp]
-declare zdiv_neg_neg [of "integ_of (v)" "integ_of (w)", standard, simp]
-declare zmod_pos_pos [of "integ_of (v)" "integ_of (w)", standard, simp]
-declare zmod_neg_pos [of "integ_of (v)" "integ_of (w)", standard, simp]
-declare zmod_pos_neg [of "integ_of (v)" "integ_of (w)", standard, simp]
-declare zmod_neg_neg [of "integ_of (v)" "integ_of (w)", standard, simp]
-declare posDivAlg_eqn [of concl: "integ_of (v)" "integ_of (w)", standard, simp]
-declare negDivAlg_eqn [of concl: "integ_of (v)" "integ_of (w)", standard, simp]
+declare zdiv_pos_pos [of "integ_of (v)" "integ_of (w)", simp] for v w
+declare zdiv_neg_pos [of "integ_of (v)" "integ_of (w)", simp] for v w
+declare zdiv_pos_neg [of "integ_of (v)" "integ_of (w)", simp] for v w
+declare zdiv_neg_neg [of "integ_of (v)" "integ_of (w)", simp] for v w
+declare zmod_pos_pos [of "integ_of (v)" "integ_of (w)", simp] for v w
+declare zmod_neg_pos [of "integ_of (v)" "integ_of (w)", simp] for v w
+declare zmod_pos_neg [of "integ_of (v)" "integ_of (w)", simp] for v w
+declare zmod_neg_neg [of "integ_of (v)" "integ_of (w)", simp] for v w
+declare posDivAlg_eqn [of concl: "integ_of (v)" "integ_of (w)", simp] for v w
+declare negDivAlg_eqn [of concl: "integ_of (v)" "integ_of (w)", simp] for v w
(** Special-case simplification **)
--- a/src/ZF/Int_ZF.thy Sun Nov 20 17:57:09 2011 +0100
+++ b/src/ZF/Int_ZF.thy Sun Nov 20 20:15:02 2011 +0100
@@ -717,7 +717,7 @@
by (blast dest: zless_trans)
(* [| z $< w; ~ P ==> w $< z |] ==> P *)
-lemmas zless_asym = zless_not_sym [THEN swap, standard]
+lemmas zless_asym = zless_not_sym [THEN swap]
lemma zless_imp_zle: "z $< w ==> z $<= w"
by (simp add: zle_def)
@@ -867,16 +867,16 @@
(*"v $<= w ==> v$+z $<= w$+z"*)
-lemmas zadd_zless_mono1 = zadd_right_cancel_zless [THEN iffD2, standard]
+lemmas zadd_zless_mono1 = zadd_right_cancel_zless [THEN iffD2]
(*"v $<= w ==> z$+v $<= z$+w"*)
-lemmas zadd_zless_mono2 = zadd_left_cancel_zless [THEN iffD2, standard]
+lemmas zadd_zless_mono2 = zadd_left_cancel_zless [THEN iffD2]
(*"v $<= w ==> v$+z $<= w$+z"*)
-lemmas zadd_zle_mono1 = zadd_right_cancel_zle [THEN iffD2, standard]
+lemmas zadd_zle_mono1 = zadd_right_cancel_zle [THEN iffD2]
(*"v $<= w ==> z$+v $<= z$+w"*)
-lemmas zadd_zle_mono2 = zadd_left_cancel_zle [THEN iffD2, standard]
+lemmas zadd_zle_mono2 = zadd_left_cancel_zle [THEN iffD2]
lemma zadd_zle_mono: "[| w' $<= w; z' $<= z |] ==> w' $+ z' $<= w $+ z"
by (erule zadd_zle_mono1 [THEN zle_trans], simp)
--- a/src/ZF/List_ZF.thy Sun Nov 20 17:57:09 2011 +0100
+++ b/src/ZF/List_ZF.thy Sun Nov 20 20:15:02 2011 +0100
@@ -317,7 +317,7 @@
(** theorems about list(Collect(A,P)) -- used in Induct/Term.thy **)
(* c : list(Collect(B,P)) ==> c : list(B) *)
-lemmas list_CollectD = Collect_subset [THEN list_mono, THEN subsetD, standard]
+lemmas list_CollectD = Collect_subset [THEN list_mono, THEN subsetD]
lemma map_list_Collect: "l: list({x:A. h(x)=j(x)}) ==> map(h,l) = map(j,l)"
apply (induct_tac "l")
--- a/src/ZF/Nat_ZF.thy Sun Nov 20 17:57:09 2011 +0100
+++ b/src/ZF/Nat_ZF.thy Sun Nov 20 20:15:02 2011 +0100
@@ -57,7 +57,7 @@
done
(* nat = {0} Un {succ(x). x:nat} *)
-lemmas nat_unfold = nat_bnd_mono [THEN nat_def [THEN def_lfp_unfold], standard]
+lemmas nat_unfold = nat_bnd_mono [THEN nat_def [THEN def_lfp_unfold]]
(** Type checking of 0 and successor **)
@@ -80,7 +80,7 @@
lemma bool_subset_nat: "bool <= nat"
by (blast elim!: boolE)
-lemmas bool_into_nat = bool_subset_nat [THEN subsetD, standard]
+lemmas bool_into_nat = bool_subset_nat [THEN subsetD]
subsection{*Injectivity Properties and Induction*}
@@ -98,10 +98,10 @@
by (erule nat_induct, auto)
(* i: nat ==> 0 le i; same thing as 0<succ(i) *)
-lemmas nat_0_le = nat_into_Ord [THEN Ord_0_le, standard]
+lemmas nat_0_le = nat_into_Ord [THEN Ord_0_le]
(* i: nat ==> i le i; same thing as i<succ(i) *)
-lemmas nat_le_refl = nat_into_Ord [THEN le_refl, standard]
+lemmas nat_le_refl = nat_into_Ord [THEN le_refl]
lemma Ord_nat [iff]: "Ord(nat)"
apply (rule OrdI)
--- a/src/ZF/Perm.thy Sun Nov 20 17:57:09 2011 +0100
+++ b/src/ZF/Perm.thy Sun Nov 20 20:15:02 2011 +0100
@@ -125,7 +125,7 @@
done
text{* f: bij(A,B) ==> f: A->B *}
-lemmas bij_is_fun = bij_is_inj [THEN inj_is_fun, standard]
+lemmas bij_is_fun = bij_is_inj [THEN inj_is_fun]
lemma lam_bijective:
"[| !!x. x:A ==> c(x): B;
@@ -174,7 +174,7 @@
apply (blast intro: lam_type)
done
-lemmas id_inj = subset_refl [THEN id_subset_inj, standard]
+lemmas id_inj = subset_refl [THEN id_subset_inj]
lemma id_surj: "id(A): surj(A,A)"
apply (unfold id_def surj_def)
@@ -220,7 +220,7 @@
"[|f \<in> inj(A,B); f ` x = y; x \<in> A|] ==> converse(f) ` y = x"
by auto
-lemmas left_inverse_bij = bij_is_inj [THEN left_inverse, standard]
+lemmas left_inverse_bij = bij_is_inj [THEN left_inverse]
lemma right_inverse_lemma:
"[| f: A->B; converse(f): C->A; b: C |] ==> f`(converse(f)`b) = b"
--- a/src/ZF/QPair.thy Sun Nov 20 17:57:09 2011 +0100
+++ b/src/ZF/QPair.thy Sun Nov 20 20:15:02 2011 +0100
@@ -82,7 +82,7 @@
apply (rule sum_equal_iff)
done
-lemmas QPair_inject = QPair_iff [THEN iffD1, THEN conjE, standard, elim!]
+lemmas QPair_inject = QPair_iff [THEN iffD1, THEN conjE, elim!]
lemma QPair_inject1: "<a;b> = <c;d> ==> a=c"
by blast
@@ -249,8 +249,8 @@
(*Injection and freeness rules*)
-lemmas QInl_inject = QInl_iff [THEN iffD1, standard]
-lemmas QInr_inject = QInr_iff [THEN iffD1, standard]
+lemmas QInl_inject = QInl_iff [THEN iffD1]
+lemmas QInr_inject = QInr_iff [THEN iffD1]
lemmas QInl_neq_QInr = QInl_QInr_iff [THEN iffD1, THEN FalseE, elim!]
lemmas QInr_neq_QInl = QInr_QInl_iff [THEN iffD1, THEN FalseE, elim!]
--- a/src/ZF/QUniv.thy Sun Nov 20 17:57:09 2011 +0100
+++ b/src/ZF/QUniv.thy Sun Nov 20 20:15:02 2011 +0100
@@ -64,7 +64,7 @@
apply (rule univ_eclose_subset_quniv)
done
-lemmas univ_into_quniv = univ_subset_quniv [THEN subsetD, standard]
+lemmas univ_into_quniv = univ_subset_quniv [THEN subsetD]
lemma Pow_univ_subset_quniv: "Pow(univ(A)) <= quniv(A)"
apply (unfold quniv_def)
@@ -72,15 +72,15 @@
done
lemmas univ_subset_into_quniv =
- PowI [THEN Pow_univ_subset_quniv [THEN subsetD], standard]
+ PowI [THEN Pow_univ_subset_quniv [THEN subsetD]]
-lemmas zero_in_quniv = zero_in_univ [THEN univ_into_quniv, standard]
-lemmas one_in_quniv = one_in_univ [THEN univ_into_quniv, standard]
-lemmas two_in_quniv = two_in_univ [THEN univ_into_quniv, standard]
+lemmas zero_in_quniv = zero_in_univ [THEN univ_into_quniv]
+lemmas one_in_quniv = one_in_univ [THEN univ_into_quniv]
+lemmas two_in_quniv = two_in_univ [THEN univ_into_quniv]
lemmas A_subset_quniv = subset_trans [OF A_subset_univ univ_subset_quniv]
-lemmas A_into_quniv = A_subset_quniv [THEN subsetD, standard]
+lemmas A_into_quniv = A_subset_quniv [THEN subsetD]
(*** univ(A) closure for Quine-inspired pairs and injections ***)
@@ -97,7 +97,7 @@
done
lemmas naturals_subset_nat =
- Ord_nat [THEN Ord_is_Transset, unfolded Transset_def, THEN bspec, standard]
+ Ord_nat [THEN Ord_is_Transset, unfolded Transset_def, THEN bspec]
lemmas naturals_subset_univ =
subset_trans [OF naturals_subset_nat nat_subset_univ]
@@ -128,7 +128,7 @@
apply (erule PowD, blast)
done
-lemmas quniv_QPair_E = quniv_QPair_D [THEN conjE, standard]
+lemmas quniv_QPair_E = quniv_QPair_D [THEN conjE]
lemma quniv_QPair_iff: "<a;b> : quniv(A) <-> a: quniv(A) & b: quniv(A)"
by (blast intro: QPair_in_quniv dest: quniv_QPair_D)
@@ -153,11 +153,11 @@
lemmas nat_subset_quniv = subset_trans [OF nat_subset_univ univ_subset_quniv]
(* n:nat ==> n:quniv(A) *)
-lemmas nat_into_quniv = nat_subset_quniv [THEN subsetD, standard]
+lemmas nat_into_quniv = nat_subset_quniv [THEN subsetD]
lemmas bool_subset_quniv = subset_trans [OF bool_subset_univ univ_subset_quniv]
-lemmas bool_into_quniv = bool_subset_quniv [THEN subsetD, standard]
+lemmas bool_into_quniv = bool_subset_quniv [THEN subsetD]
(*Intersecting <a;b> with Vfrom...*)
--- a/src/ZF/Resid/Confluence.thy Sun Nov 20 17:57:09 2011 +0100
+++ b/src/ZF/Resid/Confluence.thy Sun Nov 20 20:15:02 2011 +0100
@@ -52,13 +52,13 @@
done
lemmas confluence_parallel_reduction =
- parallel_moves [THEN strip_lemma_r, THEN strip_lemma_l, standard]
+ parallel_moves [THEN strip_lemma_r, THEN strip_lemma_l]
lemma lemma1: "[|confluence(Spar_red)|]==> confluence(Sred)"
by (unfold confluence_def, blast intro: par_red_red red_par_red)
lemmas confluence_beta_reduction =
- confluence_parallel_reduction [THEN lemma1, standard]
+ confluence_parallel_reduction [THEN lemma1]
(**** Conversion ****)
--- a/src/ZF/Sum.thy Sun Nov 20 17:57:09 2011 +0100
+++ b/src/ZF/Sum.thy Sun Nov 20 20:15:02 2011 +0100
@@ -94,8 +94,8 @@
(*Injection and freeness rules*)
-lemmas Inl_inject = Inl_iff [THEN iffD1, standard]
-lemmas Inr_inject = Inr_iff [THEN iffD1, standard]
+lemmas Inl_inject = Inl_iff [THEN iffD1]
+lemmas Inr_inject = Inr_iff [THEN iffD1]
lemmas Inl_neq_Inr = Inl_Inr_iff [THEN iffD1, THEN FalseE, elim!]
lemmas Inr_neq_Inl = Inr_Inl_iff [THEN iffD1, THEN FalseE, elim!]
@@ -168,7 +168,7 @@
by blast
lemmas Part_CollectE =
- Part_Collect [THEN equalityD1, THEN subsetD, THEN CollectE, standard]
+ Part_Collect [THEN equalityD1, THEN subsetD, THEN CollectE]
lemma Part_Inl: "Part(A+B,Inl) = {Inl(x). x: A}"
by blast
--- a/src/ZF/Trancl.thy Sun Nov 20 17:57:09 2011 +0100
+++ b/src/ZF/Trancl.thy Sun Nov 20 20:15:02 2011 +0100
@@ -109,12 +109,12 @@
(* r^* = id(field(r)) Un ( r O r^* ) *)
lemmas rtrancl_unfold =
- rtrancl_bnd_mono [THEN rtrancl_def [THEN def_lfp_unfold], standard]
+ rtrancl_bnd_mono [THEN rtrancl_def [THEN def_lfp_unfold]]
(** The relation rtrancl **)
(* r^* <= field(r) * field(r) *)
-lemmas rtrancl_type = rtrancl_def [THEN def_lfp_subset, standard]
+lemmas rtrancl_type = rtrancl_def [THEN def_lfp_subset]
lemma relation_rtrancl: "relation(r^*)"
apply (simp add: relation_def)
@@ -178,7 +178,7 @@
apply (blast intro: rtrancl_into_rtrancl)
done
-lemmas rtrancl_trans = trans_rtrancl [THEN transD, standard]
+lemmas rtrancl_trans = trans_rtrancl [THEN transD]
(*elimination of rtrancl -- by induction on a special formula*)
lemma rtranclE:
@@ -203,7 +203,7 @@
lemmas trans_on_trancl = trans_trancl [THEN trans_imp_trans_on]
-lemmas trancl_trans = trans_trancl [THEN transD, standard]
+lemmas trancl_trans = trans_trancl [THEN transD]
(** Conversions between trancl and rtrancl **)
--- a/src/ZF/UNITY/AllocBase.thy Sun Nov 20 17:57:09 2011 +0100
+++ b/src/ZF/UNITY/AllocBase.thy Sun Nov 20 20:15:02 2011 +0100
@@ -313,9 +313,9 @@
done
lemmas Increasing_state_ofD1 =
- gen_Increains_state_of_eq [THEN equalityD1, THEN subsetD, standard]
+ gen_Increains_state_of_eq [THEN equalityD1, THEN subsetD]
lemmas Increasing_state_ofD2 =
- gen_Increains_state_of_eq [THEN equalityD2, THEN subsetD, standard]
+ gen_Increains_state_of_eq [THEN equalityD2, THEN subsetD]
lemma Follows_state_of_eq:
"Follows(A, r, %s. f(state_of(s)), %s. g(state_of(s))) =
@@ -324,9 +324,9 @@
done
lemmas Follows_state_ofD1 =
- Follows_state_of_eq [THEN equalityD1, THEN subsetD, standard]
+ Follows_state_of_eq [THEN equalityD1, THEN subsetD]
lemmas Follows_state_ofD2 =
- Follows_state_of_eq [THEN equalityD2, THEN subsetD, standard]
+ Follows_state_of_eq [THEN equalityD2, THEN subsetD]
lemma nat_list_inj_type: "n\<in>nat ==> nat_list_inj(n)\<in>list(nat)"
by (induct_tac "n", auto)
@@ -373,7 +373,7 @@
by (simp add: Inter_Diff_var_iff)
(* [| Finite(A); (\<forall>x\<in>var-A. b\<in>B(x)) |] ==> b\<in>Inter(RepFun(var-A, B)) *)
-lemmas Inter_var_DiffI = Inter_Diff_var_iff [THEN iffD2, standard]
+lemmas Inter_var_DiffI = Inter_Diff_var_iff [THEN iffD2]
declare Inter_var_DiffI [intro!]
--- a/src/ZF/UNITY/Constrains.thy Sun Nov 20 17:57:09 2011 +0100
+++ b/src/ZF/UNITY/Constrains.thy Sun Nov 20 20:15:02 2011 +0100
@@ -347,8 +347,8 @@
lemma AlwaysD: "F \<in> Always(A) ==> Init(F)<=A & F \<in> Stable(A)"
by (simp add: Always_def initially_def)
-lemmas AlwaysE = AlwaysD [THEN conjE, standard]
-lemmas Always_imp_Stable = AlwaysD [THEN conjunct2, standard]
+lemmas AlwaysE = AlwaysD [THEN conjE]
+lemmas Always_imp_Stable = AlwaysD [THEN conjunct2]
(*The set of all reachable states is Always*)
lemma Always_includes_reachable: "F \<in> Always(A) ==> reachable(F) <= A"
@@ -364,7 +364,7 @@
apply (blast intro: constrains_imp_Constrains)
done
-lemmas Always_reachable = invariant_reachable [THEN invariant_imp_Always, standard]
+lemmas Always_reachable = invariant_reachable [THEN invariant_imp_Always]
lemma Always_eq_invariant_reachable: "Always(A) = {F \<in> program. F \<in> invariant(reachable(F) Int A)}"
apply (simp (no_asm) add: Always_def invariant_def Stable_def Constrains_def2 stable_def initially_def)
@@ -420,7 +420,7 @@
by (blast intro: Always_Constrains_pre [THEN iffD1])
(* [| F \<in> Always(I); F \<in> A Co A' |] ==> F \<in> A Co (I Int A') *)
-lemmas Always_ConstrainsD = Always_Constrains_post [THEN iffD2, standard]
+lemmas Always_ConstrainsD = Always_Constrains_post [THEN iffD2]
(*The analogous proof of Always_LeadsTo_weaken doesn't terminate*)
lemma Always_Constrains_weaken:
@@ -451,7 +451,7 @@
(*Delete the nearest invariance assumption (which will be the second one
used by Always_Int_I) *)
-lemmas Always_thin = thin_rl [of "F \<in> Always(A)", standard]
+lemmas Always_thin = thin_rl [of "F \<in> Always(A)"]
ML
{*
--- a/src/ZF/UNITY/FP.thy Sun Nov 20 17:57:09 2011 +0100
+++ b/src/ZF/UNITY/FP.thy Sun Nov 20 20:15:02 2011 +0100
@@ -45,7 +45,7 @@
"[| \<forall>B. F \<in> stable (A Int B); st_set(A) |] ==> A \<subseteq> FP_Orig(F)"
by (unfold FP_Orig_def stable_def st_set_def, blast)
-lemmas FP_Orig_weakest = allI [THEN FP_Orig_weakest2, standard]
+lemmas FP_Orig_weakest = allI [THEN FP_Orig_weakest2]
lemma stable_FP_Int: "F \<in> program ==> F \<in> stable (FP(F) Int B)"
apply (subgoal_tac "FP (F) Int B = (\<Union>x\<in>B. FP (F) Int {x}) ")
--- a/src/ZF/UNITY/GenPrefix.thy Sun Nov 20 17:57:09 2011 +0100
+++ b/src/ZF/UNITY/GenPrefix.thy Sun Nov 20 20:15:02 2011 +0100
@@ -350,7 +350,7 @@
apply (auto simp add: trans_def)
done
-lemmas prefix_trans = trans_prefix [THEN transD, standard]
+lemmas prefix_trans = trans_prefix [THEN transD]
lemma trans_on_prefix: "trans[list(A)](prefix(A))"
apply (unfold prefix_def)
@@ -358,7 +358,7 @@
apply (auto simp add: trans_def)
done
-lemmas prefix_trans_on = trans_on_prefix [THEN trans_onD, standard]
+lemmas prefix_trans_on = trans_on_prefix [THEN trans_onD]
(* Monotonicity of "set" operator WRT prefix *)
--- a/src/ZF/UNITY/UNITY.thy Sun Nov 20 17:57:09 2011 +0100
+++ b/src/ZF/UNITY/UNITY.thy Sun Nov 20 20:15:02 2011 +0100
@@ -167,7 +167,7 @@
lemma Init_type: "Init(F)\<subseteq>state"
by (simp add: RawInit_type Init_def)
-lemmas InitD = Init_type [THEN subsetD, standard]
+lemmas InitD = Init_type [THEN subsetD]
lemma st_set_Init [iff]: "st_set(Init(F))"
apply (unfold st_set_def)
@@ -562,7 +562,7 @@
by (unfold stable_def constrains_def st_set_def, blast)
(* [| F \<in> stable(C); F \<in> (C \<inter> A) co A |] ==> F \<in> stable(C \<inter> A) *)
-lemmas stable_constrains_stable = stable_constrains_Int [THEN stableI, standard]
+lemmas stable_constrains_stable = stable_constrains_Int [THEN stableI]
subsection{*The Operator @{term invariant}*}
--- a/src/ZF/UNITY/Union.thy Sun Nov 20 17:57:09 2011 +0100
+++ b/src/ZF/UNITY/Union.thy Sun Nov 20 20:15:02 2011 +0100
@@ -427,7 +427,7 @@
lemma ok_commute: "(F ok G) <->(G ok F)"
by (auto simp add: ok_def)
-lemmas ok_sym = ok_commute [THEN iffD1, standard]
+lemmas ok_sym = ok_commute [THEN iffD1]
lemma ok_iff_OK: "OK({<0,F>,<1,G>,<2,H>}, snd) <-> (F ok G & (F Join G) ok H)"
by (simp add: ok_def Join_def OK_def Int_assoc cons_absorb
--- a/src/ZF/UNITY/WFair.thy Sun Nov 20 17:57:09 2011 +0100
+++ b/src/ZF/UNITY/WFair.thy Sun Nov 20 20:15:02 2011 +0100
@@ -182,7 +182,7 @@
(* Added by Sidi, from Misra's notes, Progress chapter, exercise number 4 *)
(* [| F \<in> program; A<=B; st_set(A); st_set(B) |] ==> A leadsTo B *)
-lemmas subset_imp_leadsTo = subset_imp_ensures [THEN leadsTo_Basis, standard]
+lemmas subset_imp_leadsTo = subset_imp_ensures [THEN leadsTo_Basis]
lemma leadsTo_Trans: "[|F \<in> A leadsTo B; F \<in> B leadsTo C |]==>F \<in> A leadsTo C"
apply (unfold leadsTo_def)
@@ -565,7 +565,7 @@
done
(* [| F \<in> program; st_set(B) |] ==> F \<in> wlt(F, B) leadsTo B *)
-lemmas wlt_leadsTo = conjI [THEN wlt_leadsTo_iff [THEN iffD2], standard]
+lemmas wlt_leadsTo = conjI [THEN wlt_leadsTo_iff [THEN iffD2]]
lemma leadsTo_subset: "F \<in> A leadsTo B ==> A <= wlt(F, B)"
apply (unfold wlt_def)
@@ -665,7 +665,7 @@
apply blast+
done
-lemmas completion = refl [THEN completion_aux, standard]
+lemmas completion = refl [THEN completion_aux]
lemma finite_completion_aux:
"[| I \<in> Fin(X); F \<in> program; st_set(C) |] ==>
--- a/src/ZF/Univ.thy Sun Nov 20 17:57:09 2011 +0100
+++ b/src/ZF/Univ.thy Sun Nov 20 20:15:02 2011 +0100
@@ -205,9 +205,9 @@
done
lemmas Vfrom_UnI1 =
- Un_upper1 [THEN subset_refl [THEN Vfrom_mono, THEN subsetD], standard]
+ Un_upper1 [THEN subset_refl [THEN Vfrom_mono, THEN subsetD]]
lemmas Vfrom_UnI2 =
- Un_upper2 [THEN subset_refl [THEN Vfrom_mono, THEN subsetD], standard]
+ Un_upper2 [THEN subset_refl [THEN Vfrom_mono, THEN subsetD]]
text{*Hard work is finding a single j:i such that {a,b}<=Vfrom(A,j)*}
lemma doubleton_in_VLimit:
@@ -242,7 +242,7 @@
subsubsection{* Closure under Disjoint Union *}
-lemmas zero_in_VLimit = Limit_has_0 [THEN ltD, THEN zero_in_Vfrom, standard]
+lemmas zero_in_VLimit = Limit_has_0 [THEN ltD, THEN zero_in_Vfrom]
lemma one_in_VLimit: "Limit(i) ==> 1 \<in> Vfrom(A,i)"
by (blast intro: nat_into_VLimit)
@@ -409,8 +409,8 @@
lemma Vset: "Vset(i) = (\<Union>j\<in>i. Pow(Vset(j)))"
by (subst Vfrom, blast)
-lemmas Vset_succ = Transset_0 [THEN Transset_Vfrom_succ, standard]
-lemmas Transset_Vset = Transset_0 [THEN Transset_Vfrom, standard]
+lemmas Vset_succ = Transset_0 [THEN Transset_Vfrom_succ]
+lemmas Transset_Vset = Transset_0 [THEN Transset_Vfrom]
subsubsection{* Characterisation of the elements of @{term "Vset(i)"} *}
@@ -579,7 +579,7 @@
apply (rule A_subset_Vfrom)
done
-lemmas A_into_univ = A_subset_univ [THEN subsetD, standard]
+lemmas A_into_univ = A_subset_univ [THEN subsetD]
subsubsection{* Closure under Unordered and Ordered Pairs *}
@@ -620,7 +620,7 @@
done
text{* n:nat ==> n:univ(A) *}
-lemmas nat_into_univ = nat_subset_univ [THEN subsetD, standard]
+lemmas nat_into_univ = nat_subset_univ [THEN subsetD]
subsubsection{* Instances for 1 and 2 *}
@@ -638,7 +638,7 @@
apply (blast intro!: zero_in_univ one_in_univ)
done
-lemmas bool_into_univ = bool_subset_univ [THEN subsetD, standard]
+lemmas bool_into_univ = bool_subset_univ [THEN subsetD]
subsubsection{* Closure under Disjoint Union *}
@@ -764,7 +764,7 @@
assumption, fast)
text{*This weaker version says a, b exist at the same level*}
-lemmas Vfrom_doubleton_D = Transset_Vfrom [THEN Transset_doubleton_D, standard]
+lemmas Vfrom_doubleton_D = Transset_Vfrom [THEN Transset_doubleton_D]
(** Using only the weaker theorem would prove <a,b> \<in> Vfrom(X,i)
implies a, b \<in> Vfrom(X,i), which is useless for induction.
--- a/src/ZF/WF.thy Sun Nov 20 17:57:09 2011 +0100
+++ b/src/ZF/WF.thy Sun Nov 20 20:15:02 2011 +0100
@@ -164,7 +164,7 @@
by (erule_tac a=a in wf_induct, blast)
(* [| wf(r); <a,x> : r; ~P ==> <x,a> : r |] ==> P *)
-lemmas wf_asym = wf_not_sym [THEN swap, standard]
+lemmas wf_asym = wf_not_sym [THEN swap]
lemma wf_on_not_refl: "[| wf[A](r); a: A |] ==> <a,a> ~: r"
by (erule_tac a=a in wf_on_induct, assumption, blast)
@@ -212,8 +212,8 @@
text{*@{term "r-``{a}"} is the set of everything under @{term a} in @{term r}*}
-lemmas underI = vimage_singleton_iff [THEN iffD2, standard]
-lemmas underD = vimage_singleton_iff [THEN iffD1, standard]
+lemmas underI = vimage_singleton_iff [THEN iffD2]
+lemmas underD = vimage_singleton_iff [THEN iffD1]
subsection{*The Predicate @{term is_recfun}*}
--- a/src/ZF/ZF.thy Sun Nov 20 17:57:09 2011 +0100
+++ b/src/ZF/ZF.thy Sun Nov 20 20:15:02 2011 +0100
@@ -417,8 +417,8 @@
lemma equality_iffI: "(!!x. x\<in>A <-> x\<in>B) ==> A = B"
by (rule equalityI, blast+)
-lemmas equalityD1 = extension [THEN iffD1, THEN conjunct1, standard]
-lemmas equalityD2 = extension [THEN iffD1, THEN conjunct2, standard]
+lemmas equalityD1 = extension [THEN iffD1, THEN conjunct1]
+lemmas equalityD2 = extension [THEN iffD1, THEN conjunct2]
lemma equalityE: "[| A = B; [| A<=B; B<=A |] ==> P |] ==> P"
by (blast dest: equalityD1 equalityD2)
@@ -568,7 +568,7 @@
apply (best dest: equalityD2)
done
-lemmas emptyE [elim!] = not_mem_empty [THEN notE, standard]
+lemmas emptyE [elim!] = not_mem_empty [THEN notE]
lemma empty_subsetI [simp]: "0 <= A"
--- a/src/ZF/Zorn.thy Sun Nov 20 17:57:09 2011 +0100
+++ b/src/ZF/Zorn.thy Sun Nov 20 20:15:02 2011 +0100
@@ -77,9 +77,9 @@
lemma increasingD2: "[| f \<in> increasing(A); x<=A |] ==> x <= f`x"
by (unfold increasing_def, blast)
-lemmas TFin_UnionI = PowI [THEN TFin.Pow_UnionI, standard]
+lemmas TFin_UnionI = PowI [THEN TFin.Pow_UnionI]
-lemmas TFin_is_subset = TFin.dom_subset [THEN subsetD, THEN PowD, standard]
+lemmas TFin_is_subset = TFin.dom_subset [THEN subsetD, THEN PowD]
text{*Structural induction on @{term "TFin(S,next)"} *}
--- a/src/ZF/equalities.thy Sun Nov 20 17:57:09 2011 +0100
+++ b/src/ZF/equalities.thy Sun Nov 20 20:15:02 2011 +0100
@@ -81,7 +81,7 @@
(*A safe special case of subset elimination, adding no new variables
[| cons(a,B) \<subseteq> C; [| a \<in> C; B \<subseteq> C |] ==> R |] ==> R *)
-lemmas cons_subsetE = cons_subset_iff [THEN iffD1, THEN conjE, standard]
+lemmas cons_subsetE = cons_subset_iff [THEN iffD1, THEN conjE]
lemma subset_empty_iff: "A\<subseteq>0 <-> A=0"
by blast
--- a/src/ZF/ex/Limit.thy Sun Nov 20 17:57:09 2011 +0100
+++ b/src/ZF/ex/Limit.thy Sun Nov 20 20:15:02 2011 +0100
@@ -994,9 +994,9 @@
(* The following three theorems have cpo asms due to THE (uniqueness). *)
-lemmas Rp_cont [TC] = embRp [THEN projpair_p_cont, standard]
-lemmas embRp_eq = embRp [THEN projpair_eq, standard]
-lemmas embRp_rel = embRp [THEN projpair_rel, standard]
+lemmas Rp_cont [TC] = embRp [THEN projpair_p_cont]
+lemmas embRp_eq = embRp [THEN projpair_eq]
+lemmas embRp_rel = embRp [THEN projpair_rel]
lemma embRp_eq_thm:
--- a/src/ZF/ex/Primes.thy Sun Nov 20 17:57:09 2011 +0100
+++ b/src/ZF/ex/Primes.thy Sun Nov 20 20:15:02 2011 +0100
@@ -40,8 +40,8 @@
"[|m dvd n; !!k. [|m \<in> nat; n \<in> nat; k \<in> nat; n = m#*k|] ==> P|] ==> P"
by (blast dest!: dvdD)
-lemmas dvd_imp_nat1 = dvdD [THEN conjunct1, standard]
-lemmas dvd_imp_nat2 = dvdD [THEN conjunct2, THEN conjunct1, standard]
+lemmas dvd_imp_nat1 = dvdD [THEN conjunct1]
+lemmas dvd_imp_nat2 = dvdD [THEN conjunct2, THEN conjunct1]
lemma dvd_0_right [simp]: "m \<in> nat ==> m dvd 0"
@@ -122,8 +122,8 @@
done
(* k dvd (m*k) *)
-lemmas dvdI1 [simp] = dvd_refl [THEN dvd_mult, standard]
-lemmas dvdI2 [simp] = dvd_refl [THEN dvd_mult2, standard]
+lemmas dvdI1 [simp] = dvd_refl [THEN dvd_mult]
+lemmas dvdI2 [simp] = dvd_refl [THEN dvd_mult2]
lemma dvd_mod_imp_dvd_raw:
"[| a \<in> nat; b \<in> nat; k dvd b; k dvd (a mod b) |] ==> k dvd a"
--- a/src/ZF/pair.thy Sun Nov 20 17:57:09 2011 +0100
+++ b/src/ZF/pair.thy Sun Nov 20 20:15:02 2011 +0100
@@ -43,17 +43,17 @@
lemma Pair_iff [simp]: "<a,b> = <c,d> <-> a=c & b=d"
by (simp add: Pair_def doubleton_eq_iff, blast)
-lemmas Pair_inject = Pair_iff [THEN iffD1, THEN conjE, standard, elim!]
+lemmas Pair_inject = Pair_iff [THEN iffD1, THEN conjE, elim!]
-lemmas Pair_inject1 = Pair_iff [THEN iffD1, THEN conjunct1, standard]
-lemmas Pair_inject2 = Pair_iff [THEN iffD1, THEN conjunct2, standard]
+lemmas Pair_inject1 = Pair_iff [THEN iffD1, THEN conjunct1]
+lemmas Pair_inject2 = Pair_iff [THEN iffD1, THEN conjunct2]
lemma Pair_not_0: "<a,b> ~= 0"
apply (unfold Pair_def)
apply (blast elim: equalityE)
done
-lemmas Pair_neq_0 = Pair_not_0 [THEN notE, standard, elim!]
+lemmas Pair_neq_0 = Pair_not_0 [THEN notE, elim!]
declare sym [THEN Pair_neq_0, elim!]
@@ -82,8 +82,8 @@
lemma SigmaI [TC,intro!]: "[| a:A; b:B(a) |] ==> <a,b> : Sigma(A,B)"
by simp
-lemmas SigmaD1 = Sigma_iff [THEN iffD1, THEN conjunct1, standard]
-lemmas SigmaD2 = Sigma_iff [THEN iffD1, THEN conjunct2, standard]
+lemmas SigmaD1 = Sigma_iff [THEN iffD1, THEN conjunct1]
+lemmas SigmaD2 = Sigma_iff [THEN iffD1, THEN conjunct2]
(*The general elimination rule*)
lemma SigmaE [elim!]:
--- a/src/ZF/upair.thy Sun Nov 20 17:57:09 2011 +0100
+++ b/src/ZF/upair.thy Sun Nov 20 20:15:02 2011 +0100
@@ -130,7 +130,7 @@
lemma cons_not_0 [simp]: "cons(a,B) ~= 0"
by (blast elim: equalityE)
-lemmas cons_neq_0 = cons_not_0 [THEN notE, standard]
+lemmas cons_neq_0 = cons_not_0 [THEN notE]
declare cons_not_0 [THEN not_sym, simp]
@@ -143,7 +143,7 @@
lemma singletonI [intro!]: "a : {a}"
by (rule consI1)
-lemmas singletonE = singleton_iff [THEN iffD1, elim_format, standard, elim!]
+lemmas singletonE = singleton_iff [THEN iffD1, elim_format, elim!]
subsection{*Descriptions*}
@@ -228,11 +228,11 @@
addsplits[split_if]
**)
-lemmas split_if_eq1 = split_if [of "%x. x = b", standard]
-lemmas split_if_eq2 = split_if [of "%x. a = x", standard]
+lemmas split_if_eq1 = split_if [of "%x. x = b"] for b
+lemmas split_if_eq2 = split_if [of "%x. a = x"] for x
-lemmas split_if_mem1 = split_if [of "%x. x : b", standard]
-lemmas split_if_mem2 = split_if [of "%x. a : x", standard]
+lemmas split_if_mem1 = split_if [of "%x. x : b"] for b
+lemmas split_if_mem2 = split_if [of "%x. a : x"] for x
lemmas split_ifs = split_if_eq1 split_if_eq2 split_if_mem1 split_if_mem2
@@ -303,7 +303,7 @@
lemma succ_not_0 [simp]: "succ(n) ~= 0"
by (blast elim!: equalityE)
-lemmas succ_neq_0 = succ_not_0 [THEN notE, standard, elim!]
+lemmas succ_neq_0 = succ_not_0 [THEN notE, elim!]
declare succ_not_0 [THEN not_sym, simp]
declare sym [THEN succ_neq_0, elim!]
@@ -312,12 +312,12 @@
lemmas succ_subsetD = succI1 [THEN [2] subsetD]
(* succ(b) ~= b *)
-lemmas succ_neq_self = succI1 [THEN mem_imp_not_eq, THEN not_sym, standard]
+lemmas succ_neq_self = succI1 [THEN mem_imp_not_eq, THEN not_sym]
lemma succ_inject_iff [simp]: "succ(m) = succ(n) <-> m=n"
by (blast elim: mem_asym elim!: equalityE)
-lemmas succ_inject = succ_inject_iff [THEN iffD1, standard, dest!]
+lemmas succ_inject = succ_inject_iff [THEN iffD1, dest!]
subsection{*Miniscoping of the Bounded Universal Quantifier*}