--- a/doc-src/TutorialI/Protocol/Event.thy Tue Feb 14 20:57:05 2012 +0100
+++ b/doc-src/TutorialI/Protocol/Event.thy Tue Feb 14 21:19:39 2012 +0100
@@ -139,8 +139,8 @@
text{*Elimination rules: derive contradictions from old Says events containing
items known to be fresh*}
lemmas knows_Spy_partsEs =
- Says_imp_knows_Spy [THEN parts.Inj, THEN revcut_rl, standard]
- parts.Body [THEN revcut_rl, standard]
+ Says_imp_knows_Spy [THEN parts.Inj, elim_format]
+ parts.Body [elim_format]
lemmas Says_imp_analz_Spy = Says_imp_knows_Spy [THEN analz.Inj]
--- a/doc-src/ZF/ZF_examples.thy Tue Feb 14 20:57:05 2012 +0100
+++ b/doc-src/ZF/ZF_examples.thy Tue Feb 14 21:19:39 2012 +0100
@@ -80,7 +80,7 @@
emptyI: "0 \<in> Fin(A)"
consI: "[| a \<in> A; b \<in> Fin(A) |] ==> cons(a,b) \<in> Fin(A)"
type_intros empty_subsetI cons_subsetI PowI
- type_elims PowD [THEN revcut_rl]
+ type_elims PowD [elim_format]
consts acc :: "i => i"
--- a/src/HOL/Auth/Event.thy Tue Feb 14 20:57:05 2012 +0100
+++ b/src/HOL/Auth/Event.thy Tue Feb 14 21:19:39 2012 +0100
@@ -138,10 +138,10 @@
text{*Elimination rules: derive contradictions from old Says events containing
items known to be fresh*}
lemmas Says_imp_parts_knows_Spy =
- Says_imp_knows_Spy [THEN parts.Inj, THEN revcut_rl]
+ Says_imp_knows_Spy [THEN parts.Inj, elim_format]
lemmas knows_Spy_partsEs =
- Says_imp_parts_knows_Spy parts.Body [THEN revcut_rl]
+ Says_imp_parts_knows_Spy parts.Body [elim_format]
lemmas Says_imp_analz_Spy = Says_imp_knows_Spy [THEN analz.Inj]
--- a/src/HOL/Auth/Smartcard/EventSC.thy Tue Feb 14 20:57:05 2012 +0100
+++ b/src/HOL/Auth/Smartcard/EventSC.thy Tue Feb 14 21:19:39 2012 +0100
@@ -237,8 +237,8 @@
text{*Elimination rules: derive contradictions from old Says events containing
items known to be fresh*}
lemmas knows_Spy_partsEs =
- Says_imp_knows_Spy [THEN parts.Inj, THEN revcut_rl]
- parts.Body [THEN revcut_rl]
+ Says_imp_knows_Spy [THEN parts.Inj, elim_format]
+ parts.Body [elim_format]
--- a/src/HOL/SET_Protocol/Event_SET.thy Tue Feb 14 20:57:05 2012 +0100
+++ b/src/HOL/SET_Protocol/Event_SET.thy Tue Feb 14 21:19:39 2012 +0100
@@ -126,8 +126,8 @@
(*Use with addSEs to derive contradictions from old Says events containing
items known to be fresh*)
lemmas knows_Spy_partsEs =
- Says_imp_knows_Spy [THEN parts.Inj, THEN revcut_rl]
- parts.Body [THEN revcut_rl]
+ Says_imp_knows_Spy [THEN parts.Inj, elim_format]
+ parts.Body [elim_format]
subsection{*The Function @{term used}*}
--- a/src/HOL/UNITY/Project.thy Tue Feb 14 20:57:05 2012 +0100
+++ b/src/HOL/UNITY/Project.thy Tue Feb 14 21:19:39 2012 +0100
@@ -544,7 +544,7 @@
"[| F\<squnion>project h UNIV G \<in> A ensures B;
G \<in> stable (extend_set h A - extend_set h B) |]
==> extend h F\<squnion>G \<in> (extend_set h A) ensures (extend_set h B)"
-apply (rule project_ensures_D_lemma [of _ UNIV, THEN revcut_rl], auto)
+apply (rule project_ensures_D_lemma [of _ UNIV, elim_format], auto)
done
lemma (in Extend) project_Ensures_D:
@@ -553,7 +553,7 @@
extend_set h B) |]
==> extend h F\<squnion>G \<in> (extend_set h A) Ensures (extend_set h B)"
apply (unfold Ensures_def)
-apply (rule project_ensures_D_lemma [THEN revcut_rl])
+apply (rule project_ensures_D_lemma [elim_format])
apply (auto simp add: project_set_reachable_extend_eq [symmetric])
done
--- a/src/ZF/AC/Hartog.thy Tue Feb 14 20:57:05 2012 +0100
+++ b/src/ZF/AC/Hartog.thy Tue Feb 14 21:19:39 2012 +0100
@@ -13,7 +13,7 @@
"Hartog(X) == LEAST i. ~ i \<lesssim> X"
lemma Ords_in_set: "\<forall>a. Ord(a) --> a \<in> X ==> P"
-apply (rule_tac X1 = "{y \<in> X. Ord (y) }" in ON_class [THEN revcut_rl])
+apply (rule_tac X = "{y \<in> X. Ord (y) }" in ON_class [elim_format])
apply fast
done
--- a/src/ZF/AC/WO6_WO1.thy Tue Feb 14 20:57:05 2012 +0100
+++ b/src/ZF/AC/WO6_WO1.thy Tue Feb 14 21:19:39 2012 +0100
@@ -526,7 +526,7 @@
apply (rule allI)
apply (case_tac "A=0")
apply (fast intro!: well_ord_Memrel nat_0I [THEN nat_into_Ord])
-apply (rule_tac x1 = A in lemma_iv [THEN revcut_rl])
+apply (rule_tac x = A in lemma_iv [elim_format])
apply (erule exE)
apply (drule WO6_imp_NN_not_empty)
apply (erule Un_subset_iff [THEN iffD1, THEN conjE])
--- a/src/ZF/Cardinal.thy Tue Feb 14 20:57:05 2012 +0100
+++ b/src/ZF/Cardinal.thy Tue Feb 14 21:19:39 2012 +0100
@@ -869,7 +869,7 @@
apply (simp add: eqpoll_0_iff, clarify)
apply (subgoal_tac "EX u. u:A")
apply (erule exE)
-apply (rule Diff_sing_eqpoll [THEN revcut_rl])
+apply (rule Diff_sing_eqpoll [elim_format])
prefer 2 apply assumption
apply assumption
apply (rule_tac b = A in cons_Diff [THEN subst], assumption)
--- a/src/ZF/Finite.thy Tue Feb 14 20:57:05 2012 +0100
+++ b/src/ZF/Finite.thy Tue Feb 14 21:19:39 2012 +0100
@@ -27,7 +27,7 @@
emptyI: "0 : Fin(A)"
consI: "[| a: A; b: Fin(A) |] ==> cons(a,b) : Fin(A)"
type_intros empty_subsetI cons_subsetI PowI
- type_elims PowD [THEN revcut_rl]
+ type_elims PowD [elim_format]
inductive
domains "FiniteFun(A,B)" <= "Fin(A*B)"