--- a/src/ZF/AC/AC16_WO4.thy Mon Mar 23 19:43:03 2015 +0100
+++ b/src/ZF/AC/AC16_WO4.thy Mon Mar 23 21:05:17 2015 +0100
@@ -295,7 +295,7 @@
apply (rule lam_type)
apply (frule ex1_superset_a [THEN theI], fast+, clarify)
apply (rule cons_eqE [of _ a])
-apply (drule_tac A = "THE c. ?P (c) " and C = y in eq_imp_Int_eq)
+apply (drule_tac A = "THE c. P (c)" and C = y for P in eq_imp_Int_eq)
apply (simp_all add: the_eq_cons)
done
--- a/src/ZF/AC/HH.thy Mon Mar 23 19:43:03 2015 +0100
+++ b/src/ZF/AC/HH.thy Mon Mar 23 21:05:17 2015 +0100
@@ -57,7 +57,7 @@
prefer 2 apply assumption+
apply (rule leI [THEN le_imp_subset, THEN subset_imp_Diff_eq, THEN ssubst],
assumption)
-apply (rule_tac t = "%z. z-?X" in subst_context)
+apply (rule_tac t = "%z. z-X" for X in subst_context)
apply (rule Diff_UN_eq_self)
apply (drule Ord_DiffE, assumption)
apply (fast elim: ltE, auto)
@@ -162,7 +162,7 @@
lemma f_subsets_imp_UN_HH_eq_x:
"\<forall>z \<in> Pow(x)-{0}. f`z \<in> Pow(z)-{0}
==> x - (\<Union>j \<in> (LEAST i. HH(f,x,i)={x}). HH(f,x,j)) = 0"
-apply (case_tac "?P \<in> {0}", fast)
+apply (case_tac "P \<in> {0}" for P, fast)
apply (drule Diff_subset [THEN PowI, THEN DiffI])
apply (drule bspec, assumption)
apply (drule f_subset_imp_HH_subset)
--- a/src/ZF/AC/WO2_AC16.thy Mon Mar 23 19:43:03 2015 +0100
+++ b/src/ZF/AC/WO2_AC16.thy Mon Mar 23 21:05:17 2015 +0100
@@ -563,7 +563,7 @@
apply (elim exE)
apply (rename_tac h)
apply (rule_tac x = "\<Union>j<a. recfunAC16 (h,f,j,a) " in exI)
-apply (rule_tac P="%z. ?Y & (\<forall>x \<in> z. ?Z (x))"
+apply (rule_tac P="%z. Y & (\<forall>x \<in> z. Z(x))" for Y Z
in bij_is_surj [THEN surj_image_eq, THEN subst], assumption)
apply (rule lemma_simp_induct)
apply (blast del: conjI notI
--- a/src/ZF/AC/WO6_WO1.thy Mon Mar 23 19:43:03 2015 +0100
+++ b/src/ZF/AC/WO6_WO1.thy Mon Mar 23 21:05:17 2015 +0100
@@ -390,7 +390,7 @@
apply (fast intro!: Ord_oadd domain_gg1 UN_gg1_eq gg1_lepoll_m)
(* case 2 *)
apply (elim oexE conjE)
-apply (rule_tac A = "f`?B" in not_emptyE, assumption)
+apply (rule_tac A = "f`B" for B in not_emptyE, assumption)
apply (rule CollectI)
apply (erule succ_natD)
apply (rule_tac x = "a++a" in exI)
--- a/src/ZF/Cardinal.thy Mon Mar 23 19:43:03 2015 +0100
+++ b/src/ZF/Cardinal.thy Mon Mar 23 21:05:17 2015 +0100
@@ -59,7 +59,7 @@
"g \<in> Y->X
==> g``(Y - f`` lfp(X, %W. X - g``(Y - f``W))) =
X - lfp(X, %W. X - g``(Y - f``W))"
-apply (rule_tac P = "%u. ?v = X-u"
+apply (rule_tac P = "%u. v = X-u" for v
in decomp_bnd_mono [THEN lfp_unfold, THEN ssubst])
apply (simp add: double_complement fun_is_rel [THEN image_subset])
done
@@ -1079,7 +1079,7 @@
prefer 2 apply (blast del: allE elim: equalityE, clarify)
apply (subgoal_tac "B = {f(u) . u \<in> A - {z}}")
apply (blast intro: Diff_sing_Finite)
-apply (thin_tac "\<forall>A. ?P(A) \<longrightarrow> Finite(A)")
+apply (thin_tac "\<forall>A. P(A) \<longrightarrow> Finite(A)" for P)
apply (rule equalityI)
apply (blast intro: elim: equalityE)
apply (blast intro: elim: equalityCE)
--- a/src/ZF/Coind/Map.thy Mon Mar 23 19:43:03 2015 +0100
+++ b/src/ZF/Coind/Map.thy Mon Mar 23 21:05:17 2015 +0100
@@ -111,7 +111,7 @@
(*Remaining subgoal*)
apply (rule excluded_middle [THEN disjE])
apply (erule image_Sigma1)
-apply (drule_tac psi = "?uu \<notin> B" in asm_rl)
+apply (drule_tac psi = "uu \<notin> B" for uu in asm_rl)
apply (auto simp add: qbeta)
done
--- a/src/ZF/Constructible/Normal.thy Mon Mar 23 19:43:03 2015 +0100
+++ b/src/ZF/Constructible/Normal.thy Mon Mar 23 21:05:17 2015 +0100
@@ -284,7 +284,7 @@
==> F(\<Union>(X)) = (\<Union>y\<in>X. F(y))"
apply (frule Ord_set_cases)
apply (erule disjE, force)
-apply (thin_tac "X=0 \<longrightarrow> ?Q", auto)
+apply (thin_tac "X=0 \<longrightarrow> Q" for Q, auto)
txt{*The trival case of @{term "\<Union>X \<in> X"}*}
apply (rule equalityI, blast intro: Ord_Union_eq_succD)
apply (simp add: mono_le_subset_def UN_subset_iff le_subset_iff)
--- a/src/ZF/Constructible/Relative.thy Mon Mar 23 19:43:03 2015 +0100
+++ b/src/ZF/Constructible/Relative.thy Mon Mar 23 21:05:17 2015 +0100
@@ -1024,9 +1024,9 @@
apply blast
txt{*Final, difficult case: the left-to-right direction of the theorem.*}
apply (insert power_ax, simp add: power_ax_def)
-apply (frule_tac x="A \<union> B" and P="\<lambda>x. rex(M,?Q(x))" in rspec)
+apply (frule_tac x="A \<union> B" and P="\<lambda>x. rex(M,Q(x))" for Q in rspec)
apply (blast, clarify)
-apply (drule_tac x=z and P="\<lambda>x. rex(M,?Q(x))" in rspec)
+apply (drule_tac x=z and P="\<lambda>x. rex(M,Q(x))" for Q in rspec)
apply assumption
apply (blast intro: cartprod_iff_lemma)
done
@@ -1035,9 +1035,9 @@
"[| M(A); M(B) |] ==> \<exists>C[M]. cartprod(M,A,B,C)"
apply (simp del: cartprod_abs add: cartprod_iff)
apply (insert power_ax, simp add: power_ax_def)
-apply (frule_tac x="A \<union> B" and P="\<lambda>x. rex(M,?Q(x))" in rspec)
+apply (frule_tac x="A \<union> B" and P="\<lambda>x. rex(M,Q(x))" for Q in rspec)
apply (blast, clarify)
-apply (drule_tac x=z and P="\<lambda>x. rex(M,?Q(x))" in rspec, auto)
+apply (drule_tac x=z and P="\<lambda>x. rex(M,Q(x))" for Q in rspec, auto)
apply (intro rexI conjI, simp+)
apply (insert cartprod_separation [of A B], simp)
done
--- a/src/ZF/Constructible/WFrec.thy Mon Mar 23 19:43:03 2015 +0100
+++ b/src/ZF/Constructible/WFrec.thy Mon Mar 23 21:05:17 2015 +0100
@@ -180,7 +180,7 @@
==> restrict(Y, r -`` {x}) = f"
apply (subgoal_tac "\<forall>y \<in> r-``{x}. \<forall>z. <y,z>:Y \<longleftrightarrow> <y,z>:f")
apply (simp (no_asm_simp) add: restrict_def)
- apply (thin_tac "rall(M,?P)")+ --{*essential for efficiency*}
+ apply (thin_tac "rall(M,P)" for P)+ --{*essential for efficiency*}
apply (frule is_recfun_type [THEN fun_is_rel], blast)
apply (frule pair_components_in_M, assumption, clarify)
apply (rule iffI)
--- a/src/ZF/Induct/Multiset.thy Mon Mar 23 19:43:03 2015 +0100
+++ b/src/ZF/Induct/Multiset.thy Mon Mar 23 21:05:17 2015 +0100
@@ -363,7 +363,7 @@
lemma msize_eq_0_iff: "multiset(M) ==> msize(M)=#0 \<longleftrightarrow> M=0"
apply (simp add: msize_def, auto)
-apply (rule_tac P = "setsum (?u,?v) \<noteq> #0" in swap)
+apply (rule_tac P = "setsum (u,v) \<noteq> #0" for u v in swap)
apply blast
apply (drule not_empty_multiset_imp_exist, assumption, clarify)
apply (subgoal_tac "Finite (mset_of (M) - {a}) ")
@@ -571,7 +571,7 @@
apply (simp add: multiset_def multiset_fun_iff)
apply (rule_tac x = A in exI, force)
apply (simp_all add: mset_of_def)
-apply (drule_tac psi = "\<forall>x \<in> A. ?u (x) " in asm_rl)
+apply (drule_tac psi = "\<forall>x \<in> A. u(x)" for u in asm_rl)
apply (drule_tac x = a in bspec)
apply (simp (no_asm_simp))
apply (subgoal_tac "cons (a, A) = A")
@@ -596,7 +596,7 @@
apply (simp (no_asm_simp) add: multiset_def multiset_fun_iff)
apply blast
apply (simp (no_asm_simp) add: mset_of_def)
-apply (drule_tac b = "if ?u then ?v else ?w" in sym, simp_all)
+apply (drule_tac b = "if u then v else w" for u v w in sym, simp_all)
apply (subgoal_tac "{x \<in> A - {a} . 0 < funrestrict (M, A - {x}) ` x} = A - {a}")
apply (auto intro!: setsum_cong simp add: zdiff_eq_iff zadd_commute multiset_def multiset_fun_iff mset_of_def)
done
@@ -815,7 +815,7 @@
apply (subgoal_tac "aa \<in> A")
prefer 2 apply blast
apply (drule_tac x = "M0 +# M" and P =
- "%x. x \<in> acc(multirel1(A, r)) \<longrightarrow> ?Q(x)" in spec)
+ "%x. x \<in> acc(multirel1(A, r)) \<longrightarrow> Q(x)" for Q in spec)
apply (simp add: munion_assoc [symmetric])
(* subgoal 3 \<in> additional conditions *)
apply (auto intro!: multirel1_base [THEN fieldI2] simp add: Mult_iff_multiset)
@@ -942,7 +942,7 @@
apply (simp add: mdiff_union_single_conv melem_diff_single, clarify)
apply (erule disjE, simp)
apply (erule disjE, simp)
-apply (drule_tac x = a and P = "%x. x :# Ka \<longrightarrow> ?Q(x)" in spec)
+apply (drule_tac x = a and P = "%x. x :# Ka \<longrightarrow> Q(x)" for Q in spec)
apply clarify
apply (rule_tac x = xa in exI)
apply (simp (no_asm_simp))
@@ -1005,7 +1005,7 @@
apply (drule sym, rotate_tac -1, simp)
apply (erule_tac V = "$# x = msize (J') " in thin_rl)
apply (frule_tac M = K and P = "%x. <x,a> \<in> r" in multiset_partition)
-apply (erule_tac P = "\<forall>k \<in> mset_of (K) . ?P (k) " in rev_mp)
+apply (erule_tac P = "\<forall>k \<in> mset_of (K) . P(k)" for P in rev_mp)
apply (erule ssubst)
apply (simp add: Ball_def, auto)
apply (subgoal_tac "< (I +# {# x \<in> K. <x, a> \<in> r#}) +# {# x \<in> K. <x, a> \<notin> r#}, (I +# {# x \<in> K. <x, a> \<in> r#}) +# J'> \<in> multirel(A, r) ")
@@ -1119,7 +1119,7 @@
lemma munion_multirel_mono1:
"[|<M, N> \<in> multirel(A, r); K \<in> Mult(A)|] ==> <M +# K, N +# K> \<in> multirel(A, r)"
apply (frule multirel_type [THEN subsetD])
-apply (rule_tac P = "%x. <x,?u> \<in> multirel(A, r) " in munion_commute [THEN subst])
+apply (rule_tac P = "%x. <x,u> \<in> multirel(A, r)" for u in munion_commute [THEN subst])
apply (subst munion_commute [of N])
apply (rule munion_multirel_mono2)
apply (auto simp add: Mult_iff_multiset)
--- a/src/ZF/Induct/Mutil.thy Mon Mar 23 19:43:03 2015 +0100
+++ b/src/ZF/Induct/Mutil.thy Mon Mar 23 21:05:17 2015 +0100
@@ -147,7 +147,7 @@
==> t' \<notin> tiling(domino)"
apply (rule notI)
apply (drule tiling_domino_0_1)
- apply (erule_tac x = "|?A|" in eq_lt_E)
+ apply (erule_tac x = "|A|" for A in eq_lt_E)
apply (subgoal_tac "t \<in> tiling (domino)")
prefer 2 (*Requires a small simpset that won't move the succ applications*)
apply (simp only: nat_succI add_type dominoes_tile_matrix)
--- a/src/ZF/Induct/Primrec.thy Mon Mar 23 19:43:03 2015 +0100
+++ b/src/ZF/Induct/Primrec.thy Mon Mar 23 21:05:17 2015 +0100
@@ -334,7 +334,7 @@
apply (simp add: add_le_self [THEN ack_lt_mono1])
txt {* ind step *}
apply (rule succ_leI [THEN lt_trans1])
- apply (rule_tac j = "g ` ?ll #+ ?mm" in lt_trans1)
+ apply (rule_tac j = "g ` ll #+ mm" for ll mm in lt_trans1)
apply (erule_tac [2] bspec)
apply (rule nat_le_refl [THEN add_le_mono])
apply typecheck
--- a/src/ZF/Int_ZF.thy Mon Mar 23 19:43:03 2015 +0100
+++ b/src/ZF/Int_ZF.thy Mon Mar 23 21:05:17 2015 +0100
@@ -661,7 +661,7 @@
apply (simp add: zless_def znegative_def zdiff_def int_def)
apply (auto dest!: less_imp_succ_add simp add: zadd zminus int_of_def)
apply (rule_tac x = k in bexI)
-apply (erule_tac i="succ (?v)" in add_left_cancel, auto)
+apply (erule_tac i="succ (v)" for v in add_left_cancel, auto)
done
lemma zless_imp_succ_zadd:
--- a/src/ZF/Order.thy Mon Mar 23 19:43:03 2015 +0100
+++ b/src/ZF/Order.thy Mon Mar 23 21:05:17 2015 +0100
@@ -670,8 +670,8 @@
apply (auto simp: subset_def preorder_on_def refl_def vimage_def image_def)
apply blast
unfolding trans_on_def
- apply (erule_tac P = "(\<lambda>x. \<forall>y\<in>field(?r).
- \<forall>z\<in>field(?r). \<langle>x, y\<rangle> \<in> ?r \<longrightarrow> \<langle>y, z\<rangle> \<in> ?r \<longrightarrow> \<langle>x, z\<rangle> \<in> ?r)" in rev_ballE)
+ apply (erule_tac P = "(\<lambda>x. \<forall>y\<in>field(r).
+ \<forall>z\<in>field(r). \<langle>x, y\<rangle> \<in> r \<longrightarrow> \<langle>y, z\<rangle> \<in> r \<longrightarrow> \<langle>x, z\<rangle> \<in> r)" for r in rev_ballE)
(* instance obtained from proof term generated by best *)
apply best
apply blast
--- a/src/ZF/Resid/Residuals.thy Mon Mar 23 19:43:03 2015 +0100
+++ b/src/ZF/Resid/Residuals.thy Mon Mar 23 21:05:17 2015 +0100
@@ -129,7 +129,7 @@
subst_rec(v1 |> v2, u1 |> u2,n))"
apply (erule Scomp.induct, safe)
apply (simp_all add: lift_rec_Var subst_Var residuals_lift_rec)
-apply (drule_tac psi = "\<forall>x.?P (x) " in asm_rl)
+apply (drule_tac psi = "\<forall>x. P(x)" for P in asm_rl)
apply (simp add: substitution)
done
@@ -159,7 +159,7 @@
lemma preservation [rule_format]:
"u ~ v ==> regular(v) \<longrightarrow> u|>v = (u un v)|>v"
apply (erule Scomp.induct, safe)
-apply (drule_tac [3] psi = "Fun (?u) |> ?v = ?w" in asm_rl)
+apply (drule_tac [3] psi = "Fun (u) |> v = w" for u v w in asm_rl)
apply (auto simp add: union_preserve_comp comp_sym_iff)
done
--- a/src/ZF/Tools/induct_tacs.ML Mon Mar 23 19:43:03 2015 +0100
+++ b/src/ZF/Tools/induct_tacs.ML Mon Mar 23 21:05:17 2015 +0100
@@ -9,8 +9,10 @@
signature DATATYPE_TACTICS =
sig
- val induct_tac: Proof.context -> string -> int -> tactic
- val exhaust_tac: Proof.context -> string -> int -> tactic
+ val exhaust_tac: Proof.context -> string -> (binding * string option * mixfix) list ->
+ int -> tactic
+ val induct_tac: Proof.context -> string -> (binding * string option * mixfix) list ->
+ int -> tactic
val rep_datatype_i: thm -> thm -> thm list -> thm list -> theory -> theory
val rep_datatype: Facts.ref * Token.src list -> Facts.ref * Token.src list ->
(Facts.ref * Token.src list) list -> (Facts.ref * Token.src list) list -> theory -> theory
@@ -88,7 +90,7 @@
(2) exhaustion works for VARIABLES in the premises, not general terms
**)
-fun exhaust_induct_tac exh ctxt var i state = SUBGOAL (fn _ =>
+fun exhaust_induct_tac exh ctxt var fixes i state = SUBGOAL (fn _ =>
let
val thy = Proof_Context.theory_of ctxt
val ({context = ctxt', asms, ...}, _) = Subgoal.focus ctxt i state
@@ -101,11 +103,11 @@
[] => error "induction is not available for this datatype"
| major::_ => FOLogic.dest_Trueprop major)
in
- Rule_Insts.eres_inst_tac ctxt [((ixn, Position.none), var)] [] rule i
+ Rule_Insts.eres_inst_tac ctxt [((ixn, Position.none), var)] fixes rule i
end
handle Find_tname msg =>
if exh then (*try boolean case analysis instead*)
- case_tac ctxt var [] i
+ case_tac ctxt var fixes i
else error msg) i state;
val exhaust_tac = exhaust_induct_tac true;
@@ -177,12 +179,12 @@
val _ =
Theory.setup
(Method.setup @{binding induct_tac}
- (Args.goal_spec -- Scan.lift Args.name >>
- (fn (quant, s) => fn ctxt => SIMPLE_METHOD'' quant (induct_tac ctxt s)))
+ (Args.goal_spec -- Scan.lift (Args.name -- Parse.for_fixes) >>
+ (fn (quant, (s, xs)) => fn ctxt => SIMPLE_METHOD'' quant (induct_tac ctxt s xs)))
"induct_tac emulation (dynamic instantiation!)" #>
Method.setup @{binding case_tac}
- (Args.goal_spec -- Scan.lift Args.name >>
- (fn (quant, s) => fn ctxt => SIMPLE_METHOD'' quant (exhaust_tac ctxt s)))
+ (Args.goal_spec -- Scan.lift (Args.name -- Parse.for_fixes) >>
+ (fn (quant, (s, xs)) => fn ctxt => SIMPLE_METHOD'' quant (exhaust_tac ctxt s xs)))
"datatype case_tac emulation (dynamic instantiation!)");
--- a/src/ZF/UNITY/AllocImpl.thy Mon Mar 23 19:43:03 2015 +0100
+++ b/src/ZF/UNITY/AllocImpl.thy Mon Mar 23 21:05:17 2015 +0100
@@ -167,8 +167,8 @@
apply (drule_tac f = "lift (rel) " in preserves_imp_eq)
apply assumption+
apply (force dest: ActsD)
-apply (erule_tac V = "\<forall>x \<in> Acts (alloc_prog) \<union> Acts (G). ?P(x)" in thin_rl)
-apply (erule_tac V = "alloc_prog \<in> stable (?u)" in thin_rl)
+apply (erule_tac V = "\<forall>x \<in> Acts (alloc_prog) \<union> Acts (G). P(x)" for P in thin_rl)
+apply (erule_tac V = "alloc_prog \<in> stable (u)" for u in thin_rl)
apply (drule_tac a = "xc`rel" and f = "lift (rel)" in Increasing_imp_Stable)
apply (auto simp add: Stable_def Constrains_def constrains_def)
apply (drule bspec, force)
@@ -219,7 +219,7 @@
transient({s\<in>state. k \<le> length(s`rel)} \<inter>
{s\<in>state. succ(s`NbR) = k})"
apply auto
-apply (erule_tac V = "G\<notin>?u" in thin_rl)
+apply (erule_tac V = "G\<notin>u" for u in thin_rl)
apply (rule_tac act = alloc_rel_act in transientI)
apply (simp (no_asm) add: alloc_prog_def [THEN def_prg_Acts])
apply (simp (no_asm) add: alloc_rel_act_def [THEN def_act_eq, THEN act_subset])
@@ -329,7 +329,7 @@
{s\<in>state. k < length(s`ask)} \<inter> {s\<in>state. length(s`giv)=k}
Ensures {s\<in>state. ~ k <length(s`ask)} \<union> {s\<in>state. length(s`giv) \<noteq> k}"
apply (rule EnsuresI, auto)
-apply (erule_tac [2] V = "G\<notin>?u" in thin_rl)
+apply (erule_tac [2] V = "G\<notin>u" for u in thin_rl)
apply (rule_tac [2] act = alloc_giv_act in transientI)
prefer 2
apply (simp add: alloc_prog_def [THEN def_prg_Acts])
@@ -573,7 +573,7 @@
apply (rule LeadsTo_weaken_R)
apply (rule Always_LeadsToD [OF safety length_ask_giv], assumption+, clarify)
apply (simp add: INT_iff)
-apply (drule_tac x = "length(x ` giv)" and P = "%x. ?f (x) \<le> NbT" in bspec)
+apply (drule_tac x = "length(x ` giv)" and P = "%x. f (x) \<le> NbT" for f in bspec)
apply simp
apply (blast intro: le_trans)
done
--- a/src/ZF/UNITY/Comp.thy Mon Mar 23 19:43:03 2015 +0100
+++ b/src/ZF/UNITY/Comp.thy Mon Mar 23 21:05:17 2015 +0100
@@ -305,8 +305,8 @@
(*The G case remains*)
apply (auto dest: ActsD simp add: preserves_def stable_def constrains_def ball_conj_distrib all_conj_distrib)
(*We have a G-action, so delete assumptions about F-actions*)
-apply (erule_tac V = "\<forall>act \<in> Acts (F) . ?P (act)" in thin_rl)
-apply (erule_tac V = "\<forall>k\<in>A. \<forall>act \<in> Acts (F) . ?P (k,act)" in thin_rl)
+apply (erule_tac V = "\<forall>act \<in> Acts (F). P (act)" for P in thin_rl)
+apply (erule_tac V = "\<forall>k\<in>A. \<forall>act \<in> Acts (F) . P (k,act)" for P in thin_rl)
apply (subgoal_tac "f (x) = f (xa) ")
apply (auto dest!: bspec)
done
--- a/src/ZF/UNITY/Distributor.thy Mon Mar 23 19:43:03 2015 +0100
+++ b/src/ZF/UNITY/Distributor.thy Mon Mar 23 21:05:17 2015 +0100
@@ -131,7 +131,7 @@
apply (subgoal_tac "length (s ` iIn) \<in> nat")
apply typecheck
apply (subgoal_tac "m \<in> nat")
-apply (drule_tac x = "nth(m, s`iIn) " and P = "%elt. ?X (elt) \<longrightarrow> elt<Nclients" in bspec)
+apply (drule_tac x = "nth(m, s`iIn) " and P = "%elt. X (elt) \<longrightarrow> elt<Nclients" for X in bspec)
apply (simp add: ltI)
apply (simp_all add: Ord_mem_iff_lt)
apply (blast dest: ltD)
--- a/src/ZF/UNITY/Follows.thy Mon Mar 23 19:43:03 2015 +0100
+++ b/src/ZF/UNITY/Follows.thy Mon Mar 23 21:05:17 2015 +0100
@@ -114,14 +114,14 @@
apply (rule single_LeadsTo_I, auto)
apply (drule_tac x = "g (sa) " and A = B in bspec)
apply auto
-apply (drule_tac x = "f (sa) " and P = "%j. F \<in> ?X (j) \<longmapsto>w ?Y (j) " in bspec)
+apply (drule_tac x = "f (sa) " and P = "%j. F \<in> X(j) \<longmapsto>w Y(j)" for X Y in bspec)
apply auto
apply (rule PSP_Stable [THEN LeadsTo_weaken], blast, blast)
apply auto
apply (force simp add: part_order_def refl_def)
apply (force simp add: part_order_def refl_def)
-apply (drule_tac x = "f1 (x) " and x1 = "f (sa) " and P2 = "%x y. \<forall>u\<in>B. ?P (x,y,u) " in bspec [THEN bspec])
-apply (drule_tac [3] x = "g (x) " and x1 = "g (sa) " and P2 = "%x y. ?P (x,y) \<longrightarrow> ?d (x,y) \<in> t" in bspec [THEN bspec])
+apply (drule_tac x = "f1 (x)" and x1 = "f (sa) " and P2 = "%x y. \<forall>u\<in>B. P (x,y,u)" for P in bspec [THEN bspec])
+apply (drule_tac [3] x = "g (x) " and x1 = "g (sa) " and P2 = "%x y. P (x,y) \<longrightarrow> d (x,y) \<in> t" for P d in bspec [THEN bspec])
apply auto
apply (rule_tac b = "h (f (sa), g (sa))" and A = C in trans_onD)
apply (auto simp add: part_order_def)
@@ -135,7 +135,7 @@
F:{x \<in> state. <k, h(f(x), g(x))> \<in> t} LeadsTo {x \<in> state. <k, h(f(x), g1(x))> \<in> t}"
apply (unfold mono2_def Increasing_def)
apply (rule single_LeadsTo_I, auto)
-apply (drule_tac x = "f (sa) " and P = "%k. F \<in> Stable (?X (k))" in bspec)
+apply (drule_tac x = "f (sa) " and P = "%k. F \<in> Stable (X (k))" for X in bspec)
apply auto
apply (drule_tac x = "g (sa) " in bspec)
apply auto
@@ -144,7 +144,7 @@
apply (force simp add: part_order_def refl_def)
apply (force simp add: part_order_def refl_def)
apply (drule_tac x = "f (x) " and x1 = "f (sa) " in bspec [THEN bspec])
-apply (drule_tac [3] x = "g1 (x) " and x1 = "g (sa) " and P2 = "%x y. ?P (x,y) \<longrightarrow> ?d (x,y) \<in> t" in bspec [THEN bspec])
+apply (drule_tac [3] x = "g1 (x) " and x1 = "g (sa) " and P2 = "%x y. P (x,y) \<longrightarrow> d (x,y) \<in> t" for P d in bspec [THEN bspec])
apply auto
apply (rule_tac b = "h (f (sa), g (sa))" and A = C in trans_onD)
apply (auto simp add: part_order_def)
--- a/src/ZF/UNITY/GenPrefix.thy Mon Mar 23 19:43:03 2015 +0100
+++ b/src/ZF/UNITY/GenPrefix.thy Mon Mar 23 21:05:17 2015 +0100
@@ -281,9 +281,9 @@
apply (simp_all add: nth_append length_type length_app)
apply (rule conjI)
apply (blast intro: gen_prefix.append)
-apply (erule_tac V = "length (xs) < length (ys) \<longrightarrow>?u" in thin_rl)
+apply (erule_tac V = "length (xs) < length (ys) \<longrightarrow>u" for u in thin_rl)
apply (erule_tac a = zs in list.cases, auto)
-apply (rule_tac P1 = "%x. <?u (x), ?v>:?w" in nat_diff_split [THEN iffD2])
+apply (rule_tac P1 = "%x. <u(x), v>:w" for u v w in nat_diff_split [THEN iffD2])
apply auto
apply (simplesubst append_cons_conv)
apply (rule_tac [2] gen_prefix.append)
@@ -407,7 +407,7 @@
declare same_prefix_prefix [simp]
lemma same_prefix_prefix_Nil: "xs \<in> list(A) ==> <xs@ys,xs> \<in> prefix(A) \<longleftrightarrow> (<ys,[]> \<in> prefix(A))"
-apply (rule_tac P = "%x. <?u, x>:?v \<longleftrightarrow> ?w (x) " in app_right_Nil [THEN subst])
+apply (rule_tac P = "%x. <u, x>:v \<longleftrightarrow> w(x)" for u v w in app_right_Nil [THEN subst])
apply (rule_tac [2] same_prefix_prefix, auto)
done
declare same_prefix_prefix_Nil [simp]
--- a/src/ZF/UNITY/Increasing.thy Mon Mar 23 19:43:03 2015 +0100
+++ b/src/ZF/UNITY/Increasing.thy Mon Mar 23 21:05:17 2015 +0100
@@ -67,8 +67,8 @@
apply (drule_tac x = "f (xb) " in bspec)
apply (rotate_tac [2] -1)
apply (drule_tac [2] x = act in bspec, simp_all)
-apply (drule_tac A = "act``?u" and c = xa in subsetD, blast)
-apply (drule_tac x = "f (xa) " and x1 = "f (xb) " in bspec [THEN bspec])
+apply (drule_tac A = "act``u" and c = xa for u in subsetD, blast)
+apply (drule_tac x = "f(xa) " and x1 = "f(xb)" in bspec [THEN bspec])
apply (rule_tac [3] b = "g (f (xb))" and A = B in trans_onD)
apply simp_all
done
@@ -137,8 +137,8 @@
apply clarify
apply (rotate_tac -2)
apply (drule_tac x = act in bspec)
-apply (drule_tac [2] A = "act``?u" and c = xa in subsetD, simp_all, blast)
-apply (drule_tac x = "f (xa) " and x1 = "f (xb) " in bspec [THEN bspec])
+apply (drule_tac [2] A = "act``u" and c = xa for u in subsetD, simp_all, blast)
+apply (drule_tac x = "f(xa)" and x1 = "f(xb)" in bspec [THEN bspec])
apply (rule_tac [3] b = "g (f (xb))" and A = B in trans_onD)
apply simp_all
done
@@ -181,8 +181,8 @@
apply (drule_tac x = act in bspec)
apply (rotate_tac [2] -3)
apply (drule_tac [2] x = act in bspec, simp_all)
-apply (drule_tac A = "act``?u" and c = xa in subsetD)
-apply (drule_tac [2] A = "act``?u" and c = xa in subsetD, blast, blast)
+apply (drule_tac A = "act``u" and c = xa for u in subsetD)
+apply (drule_tac [2] A = "act``u" and c = xa for u in subsetD, blast, blast)
apply (rotate_tac -4)
apply (drule_tac x = "f (xa) " and x1 = "f (xb) " in bspec [THEN bspec])
apply (rotate_tac [3] -1)
@@ -213,8 +213,8 @@
apply (drule_tac x = act in bspec)
apply (rotate_tac [2] -3)
apply (drule_tac [2] x = act in bspec, simp_all)
-apply (drule_tac A = "act``?u" and c = x in subsetD)
-apply (drule_tac [2] A = "act``?u" and c = x in subsetD, blast, blast)
+apply (drule_tac A = "act``u" and c = x for u in subsetD)
+apply (drule_tac [2] A = "act``u" and c = x for u in subsetD, blast, blast)
apply (rotate_tac -9)
apply (drule_tac x = "f (x) " and x1 = "f (xa) " in bspec [THEN bspec])
apply (rotate_tac [3] -1)
--- a/src/ZF/UNITY/Merge.thy Mon Mar 23 19:43:03 2015 +0100
+++ b/src/ZF/UNITY/Merge.thy Mon Mar 23 21:05:17 2015 +0100
@@ -166,7 +166,7 @@
apply (subgoal_tac "xa \<in> nat")
apply (simp_all add: Ord_mem_iff_lt)
prefer 2 apply (blast intro: lt_trans)
-apply (drule_tac x = "nth (xa, x`iOut)" and P = "%elt. ?X (elt) \<longrightarrow> elt<Nclients" in bspec)
+apply (drule_tac x = "nth (xa, x`iOut)" and P = "%elt. X (elt) \<longrightarrow> elt<Nclients" for X in bspec)
apply (simp add: ltI nat_into_Ord)
apply (blast dest: ltD)
done
--- a/src/ZF/UNITY/WFair.thy Mon Mar 23 19:43:03 2015 +0100
+++ b/src/ZF/UNITY/WFair.thy Mon Mar 23 21:05:17 2015 +0100
@@ -517,7 +517,7 @@
apply (unfold field_def)
apply (simp add: measure_def)
apply (rule equalityI, force, clarify)
-apply (erule_tac V = "x\<notin>range (?y) " in thin_rl)
+apply (erule_tac V = "x\<notin>range (y)" for y in thin_rl)
apply (erule nat_induct)
apply (rule_tac [2] b = "succ (succ (xa))" in domainI)
apply (rule_tac b = "succ (0) " in domainI)
--- a/src/ZF/WF.thy Mon Mar 23 19:43:03 2015 +0100
+++ b/src/ZF/WF.thy Mon Mar 23 21:05:17 2015 +0100
@@ -230,7 +230,7 @@
"[| is_recfun(r,a,H,f); <x,a>:r |] ==> f`x = H(x, restrict(f,r-``{x}))"
apply (unfold is_recfun_def)
txt{*replace f only on the left-hand side*}
-apply (erule_tac P = "%x.?t(x) = ?u" in ssubst)
+apply (erule_tac P = "%x. t(x) = u" for t u in ssubst)
apply (simp add: underI)
done
@@ -244,7 +244,7 @@
apply (intro impI)
apply (elim ssubst)
apply (simp (no_asm_simp) add: vimage_singleton_iff restrict_def)
-apply (rule_tac t = "%z. H (?x,z) " in subst_context)
+apply (rule_tac t = "%z. H (x, z)" for x in subst_context)
apply (subgoal_tac "\<forall>y\<in>r-``{x}. \<forall>z. <y,z>:f \<longleftrightarrow> <y,z>:g")
apply (blast dest: transD)
apply (simp add: apply_iff)
@@ -291,7 +291,7 @@
apply (rule lam_cong [OF refl])
apply (drule underD)
apply (fold is_recfun_def)
-apply (rule_tac t = "%z. H(?x,z)" in subst_context)
+apply (rule_tac t = "%z. H(x, z)" for x in subst_context)
apply (rule fun_extension)
apply (blast intro: is_recfun_type)
apply (rule lam_type [THEN restrict_type2])
--- a/src/ZF/Zorn.thy Mon Mar 23 19:43:03 2015 +0100
+++ b/src/ZF/Zorn.thy Mon Mar 23 21:05:17 2015 +0100
@@ -469,7 +469,7 @@
apply (erule lamE) apply simp
apply assumption
- apply (thin_tac "C \<subseteq> ?X")
+ apply (thin_tac "C \<subseteq> X" for X)
apply (fast elim: lamE)
done
have "?A \<in> Chain(r)"
--- a/src/ZF/ex/Limit.thy Mon Mar 23 19:43:03 2015 +0100
+++ b/src/ZF/ex/Limit.thy Mon Mar 23 21:05:17 2015 +0100
@@ -1833,8 +1833,8 @@
apply (rename_tac [5] y)
apply (rule_tac [5] P =
"%z. rel(DD`succ(y),
- (ee`y O Rp(?DD(y)`y,?DD(y)`succ(y),?ee(y)`y)) ` (x`succ(y)),
- z)"
+ (ee`y O Rp(DD'(y)`y,DD'(y)`succ(y),ee'(y)`y)) ` (x`succ(y)),
+ z)" for DD' ee'
in id_conv [THEN subst])
apply (rule_tac [6] rel_cf)
(* Dinf and cont_fun doesn't go well together, both Pi(_,%x._). *)
--- a/src/ZF/ex/Primes.thy Mon Mar 23 19:43:03 2015 +0100
+++ b/src/ZF/ex/Primes.thy Mon Mar 23 21:05:17 2015 +0100
@@ -93,7 +93,7 @@
lemma gcd_non_0_raw:
"[| 0<n; n \<in> nat |] ==> gcd(m,n) = gcd(n, m mod n)"
apply (simp add: gcd_def)
-apply (rule_tac P = "%z. ?left (z) = ?right" in transrec [THEN ssubst])
+apply (rule_tac P = "%z. left (z) = right" for left right in transrec [THEN ssubst])
apply (simp add: ltD [THEN mem_imp_not_eq, THEN not_sym]
mod_less_divisor [THEN ltD])
done