src/HOL/Auth/Message.thy
changeset 14145 2e31b8cc8788
parent 14126 28824746d046
child 14181 942db403d4bb
     1.1 --- a/src/HOL/Auth/Message.thy	Fri Aug 08 15:05:11 2003 +0200
     1.2 +++ b/src/HOL/Auth/Message.thy	Tue Aug 12 13:35:03 2003 +0200
     1.3 @@ -683,10 +683,10 @@
     1.4  done
     1.5  
     1.6  lemma analz_conj_parts [simp]: "(X \<in> analz H & X \<in> parts H) = (X \<in> analz H)"
     1.7 -by (blast intro: analz_subset_parts [THEN [2] rev_subsetD])
     1.8 +by (blast intro: analz_subset_parts [THEN subsetD])
     1.9  
    1.10  lemma analz_disj_parts [simp]: "(X \<in> analz H | X \<in> parts H) = (X \<in> parts H)"
    1.11 -by (blast intro: analz_subset_parts [THEN [2] rev_subsetD])
    1.12 +by (blast intro: analz_subset_parts [THEN subsetD])
    1.13  
    1.14  (*Without this equation, other rules for synth and analz would yield
    1.15    redundant cases*)
    1.16 @@ -994,6 +994,8 @@
    1.17  apply (simp add: parts_mono) 
    1.18  done
    1.19  
    1.20 +lemmas Fake_parts_sing_imp_Un = Fake_parts_sing [THEN [2] rev_subsetD]
    1.21 +
    1.22  method_setup spy_analz = {*
    1.23      Method.ctxt_args (fn ctxt =>
    1.24          Method.METHOD (fn facts =>