prefer high-level elim_format;
authorwenzelm
Tue Feb 14 21:19:39 2012 +0100 (2012-02-14)
changeset 464712289a3869c88
parent 46470 b0331b0d33a3
child 46472 06ca0a613687
prefer high-level elim_format;
doc-src/TutorialI/Protocol/Event.thy
doc-src/ZF/ZF_examples.thy
src/HOL/Auth/Event.thy
src/HOL/Auth/Smartcard/EventSC.thy
src/HOL/SET_Protocol/Event_SET.thy
src/HOL/UNITY/Project.thy
src/ZF/AC/Hartog.thy
src/ZF/AC/WO6_WO1.thy
src/ZF/Cardinal.thy
src/ZF/Finite.thy
     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)"