Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Auth/Message.thy
changeset 14145 2e31b8cc8788
parent 14126 28824746d046
child 14181 942db403d4bb 
--- a/src/HOL/Auth/Message.thy	Fri Aug 08 15:05:11 2003 +0200
+++ b/src/HOL/Auth/Message.thy	Tue Aug 12 13:35:03 2003 +0200
@@ -683,10 +683,10 @@
 done
 
 lemma analz_conj_parts [simp]: "(X \<in> analz H & X \<in> parts H) = (X \<in> analz H)"
-by (blast intro: analz_subset_parts [THEN [2] rev_subsetD])
+by (blast intro: analz_subset_parts [THEN subsetD])
 
 lemma analz_disj_parts [simp]: "(X \<in> analz H | X \<in> parts H) = (X \<in> parts H)"
-by (blast intro: analz_subset_parts [THEN [2] rev_subsetD])
+by (blast intro: analz_subset_parts [THEN subsetD])
 
 (*Without this equation, other rules for synth and analz would yield
   redundant cases*)
@@ -994,6 +994,8 @@
 apply (simp add: parts_mono) 
 done
 
+lemmas Fake_parts_sing_imp_Un = Fake_parts_sing [THEN [2] rev_subsetD]
+
 method_setup spy_analz = {*
     Method.ctxt_args (fn ctxt =>
         Method.METHOD (fn facts =>
isabelle