# HG changeset patch
# User wenzelm
# Date 1329250779 -3600
# Node ID 2289a3869c885f6ab1a0bc7e116d3456f4e08291
# Parent  b0331b0d33a39c780997f4390047900305629021
prefer high-level elim_format;

diff -r b0331b0d33a3 -r 2289a3869c88 doc-src/TutorialI/Protocol/Event.thy
--- 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]
 
diff -r b0331b0d33a3 -r 2289a3869c88 doc-src/ZF/ZF_examples.thy
--- 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"
diff -r b0331b0d33a3 -r 2289a3869c88 src/HOL/Auth/Event.thy
--- 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]
 
diff -r b0331b0d33a3 -r 2289a3869c88 src/HOL/Auth/Smartcard/EventSC.thy
--- 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]
 
 
 
diff -r b0331b0d33a3 -r 2289a3869c88 src/HOL/SET_Protocol/Event_SET.thy
--- 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}*}
diff -r b0331b0d33a3 -r 2289a3869c88 src/HOL/UNITY/Project.thy
--- 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
 
diff -r b0331b0d33a3 -r 2289a3869c88 src/ZF/AC/Hartog.thy
--- 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
 
diff -r b0331b0d33a3 -r 2289a3869c88 src/ZF/AC/WO6_WO1.thy
--- 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])
diff -r b0331b0d33a3 -r 2289a3869c88 src/ZF/Cardinal.thy
--- 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)
diff -r b0331b0d33a3 -r 2289a3869c88 src/ZF/Finite.thy
--- 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)"