# HG changeset patch
# User paulson
# Date 1158757906 -7200
# Node ID 742c30fc3fcbce521540a71dded9e7b1e64298e9
# Parent  680b58597f653d125a22baef62724cc7c05f7e95
tidied

diff -r 680b58597f65 -r 742c30fc3fcb src/HOL/Auth/Message.thy
--- a/src/HOL/Auth/Message.thy	Wed Sep 20 14:02:41 2006 +0200
+++ b/src/HOL/Auth/Message.thy	Wed Sep 20 15:11:46 2006 +0200
@@ -941,8 +941,7 @@
      "X \<in> synth (analz H) ==> parts{X} \<subseteq> synth (analz H) \<union> parts H";
 apply (rule subset_trans) 
  apply (erule_tac [2] Fake_parts_insert)
-apply (rule parts_mono)  
-apply (blast intro: elim:); 
+apply (rule parts_mono, blast)
 done
 
 lemmas Fake_parts_sing_imp_Un = Fake_parts_sing [THEN [2] rev_subsetD]