1.1 --- a/doc-src/TutorialI/Protocol/Event.thy Tue Feb 14 20:57:05 2012 +0100
1.2 +++ b/doc-src/TutorialI/Protocol/Event.thy Tue Feb 14 21:19:39 2012 +0100
1.3 @@ -139,8 +139,8 @@
1.4 text{*Elimination rules: derive contradictions from old Says events containing
1.5 items known to be fresh*}
1.6 lemmas knows_Spy_partsEs =
1.7 - Says_imp_knows_Spy [THEN parts.Inj, THEN revcut_rl, standard]
1.8 - parts.Body [THEN revcut_rl, standard]
1.9 + Says_imp_knows_Spy [THEN parts.Inj, elim_format]
1.10 + parts.Body [elim_format]
1.11
1.12 lemmas Says_imp_analz_Spy = Says_imp_knows_Spy [THEN analz.Inj]
1.13
2.1 --- a/doc-src/ZF/ZF_examples.thy Tue Feb 14 20:57:05 2012 +0100
2.2 +++ b/doc-src/ZF/ZF_examples.thy Tue Feb 14 21:19:39 2012 +0100
2.3 @@ -80,7 +80,7 @@
2.4 emptyI: "0 \<in> Fin(A)"
2.5 consI: "[| a \<in> A; b \<in> Fin(A) |] ==> cons(a,b) \<in> Fin(A)"
2.6 type_intros empty_subsetI cons_subsetI PowI
2.7 - type_elims PowD [THEN revcut_rl]
2.8 + type_elims PowD [elim_format]
2.9
2.10
2.11 consts acc :: "i => i"
3.1 --- a/src/HOL/Auth/Event.thy Tue Feb 14 20:57:05 2012 +0100
3.2 +++ b/src/HOL/Auth/Event.thy Tue Feb 14 21:19:39 2012 +0100
3.3 @@ -138,10 +138,10 @@
3.4 text{*Elimination rules: derive contradictions from old Says events containing
3.5 items known to be fresh*}
3.6 lemmas Says_imp_parts_knows_Spy =
3.7 - Says_imp_knows_Spy [THEN parts.Inj, THEN revcut_rl]
3.8 + Says_imp_knows_Spy [THEN parts.Inj, elim_format]
3.9
3.10 lemmas knows_Spy_partsEs =
3.11 - Says_imp_parts_knows_Spy parts.Body [THEN revcut_rl]
3.12 + Says_imp_parts_knows_Spy parts.Body [elim_format]
3.13
3.14 lemmas Says_imp_analz_Spy = Says_imp_knows_Spy [THEN analz.Inj]
3.15
4.1 --- a/src/HOL/Auth/Smartcard/EventSC.thy Tue Feb 14 20:57:05 2012 +0100
4.2 +++ b/src/HOL/Auth/Smartcard/EventSC.thy Tue Feb 14 21:19:39 2012 +0100
4.3 @@ -237,8 +237,8 @@
4.4 text{*Elimination rules: derive contradictions from old Says events containing
4.5 items known to be fresh*}
4.6 lemmas knows_Spy_partsEs =
4.7 - Says_imp_knows_Spy [THEN parts.Inj, THEN revcut_rl]
4.8 - parts.Body [THEN revcut_rl]
4.9 + Says_imp_knows_Spy [THEN parts.Inj, elim_format]
4.10 + parts.Body [elim_format]
4.11
4.12
4.13
5.1 --- a/src/HOL/SET_Protocol/Event_SET.thy Tue Feb 14 20:57:05 2012 +0100
5.2 +++ b/src/HOL/SET_Protocol/Event_SET.thy Tue Feb 14 21:19:39 2012 +0100
5.3 @@ -126,8 +126,8 @@
5.4 (*Use with addSEs to derive contradictions from old Says events containing
5.5 items known to be fresh*)
5.6 lemmas knows_Spy_partsEs =
5.7 - Says_imp_knows_Spy [THEN parts.Inj, THEN revcut_rl]
5.8 - parts.Body [THEN revcut_rl]
5.9 + Says_imp_knows_Spy [THEN parts.Inj, elim_format]
5.10 + parts.Body [elim_format]
5.11
5.12
5.13 subsection{*The Function @{term used}*}
6.1 --- a/src/HOL/UNITY/Project.thy Tue Feb 14 20:57:05 2012 +0100
6.2 +++ b/src/HOL/UNITY/Project.thy Tue Feb 14 21:19:39 2012 +0100
6.3 @@ -544,7 +544,7 @@
6.4 "[| F\<squnion>project h UNIV G \<in> A ensures B;
6.5 G \<in> stable (extend_set h A - extend_set h B) |]
6.6 ==> extend h F\<squnion>G \<in> (extend_set h A) ensures (extend_set h B)"
6.7 -apply (rule project_ensures_D_lemma [of _ UNIV, THEN revcut_rl], auto)
6.8 +apply (rule project_ensures_D_lemma [of _ UNIV, elim_format], auto)
6.9 done
6.10
6.11 lemma (in Extend) project_Ensures_D:
6.12 @@ -553,7 +553,7 @@
6.13 extend_set h B) |]
6.14 ==> extend h F\<squnion>G \<in> (extend_set h A) Ensures (extend_set h B)"
6.15 apply (unfold Ensures_def)
6.16 -apply (rule project_ensures_D_lemma [THEN revcut_rl])
6.17 +apply (rule project_ensures_D_lemma [elim_format])
6.18 apply (auto simp add: project_set_reachable_extend_eq [symmetric])
6.19 done
6.20
7.1 --- a/src/ZF/AC/Hartog.thy Tue Feb 14 20:57:05 2012 +0100
7.2 +++ b/src/ZF/AC/Hartog.thy Tue Feb 14 21:19:39 2012 +0100
7.3 @@ -13,7 +13,7 @@
7.4 "Hartog(X) == LEAST i. ~ i \<lesssim> X"
7.5
7.6 lemma Ords_in_set: "\<forall>a. Ord(a) --> a \<in> X ==> P"
7.7 -apply (rule_tac X1 = "{y \<in> X. Ord (y) }" in ON_class [THEN revcut_rl])
7.8 +apply (rule_tac X = "{y \<in> X. Ord (y) }" in ON_class [elim_format])
7.9 apply fast
7.10 done
7.11
8.1 --- a/src/ZF/AC/WO6_WO1.thy Tue Feb 14 20:57:05 2012 +0100
8.2 +++ b/src/ZF/AC/WO6_WO1.thy Tue Feb 14 21:19:39 2012 +0100
8.3 @@ -526,7 +526,7 @@
8.4 apply (rule allI)
8.5 apply (case_tac "A=0")
8.6 apply (fast intro!: well_ord_Memrel nat_0I [THEN nat_into_Ord])
8.7 -apply (rule_tac x1 = A in lemma_iv [THEN revcut_rl])
8.8 +apply (rule_tac x = A in lemma_iv [elim_format])
8.9 apply (erule exE)
8.10 apply (drule WO6_imp_NN_not_empty)
8.11 apply (erule Un_subset_iff [THEN iffD1, THEN conjE])
9.1 --- a/src/ZF/Cardinal.thy Tue Feb 14 20:57:05 2012 +0100
9.2 +++ b/src/ZF/Cardinal.thy Tue Feb 14 21:19:39 2012 +0100
9.3 @@ -869,7 +869,7 @@
9.4 apply (simp add: eqpoll_0_iff, clarify)
9.5 apply (subgoal_tac "EX u. u:A")
9.6 apply (erule exE)
9.7 -apply (rule Diff_sing_eqpoll [THEN revcut_rl])
9.8 +apply (rule Diff_sing_eqpoll [elim_format])
9.9 prefer 2 apply assumption
9.10 apply assumption
9.11 apply (rule_tac b = A in cons_Diff [THEN subst], assumption)
10.1 --- a/src/ZF/Finite.thy Tue Feb 14 20:57:05 2012 +0100
10.2 +++ b/src/ZF/Finite.thy Tue Feb 14 21:19:39 2012 +0100
10.3 @@ -27,7 +27,7 @@
10.4 emptyI: "0 : Fin(A)"
10.5 consI: "[| a: A; b: Fin(A) |] ==> cons(a,b) : Fin(A)"
10.6 type_intros empty_subsetI cons_subsetI PowI
10.7 - type_elims PowD [THEN revcut_rl]
10.8 + type_elims PowD [elim_format]
10.9
10.10 inductive
10.11 domains "FiniteFun(A,B)" <= "Fin(A*B)"