1.1 --- a/src/HOL/Auth/Message.thy Wed Sep 20 14:02:41 2006 +0200
1.2 +++ b/src/HOL/Auth/Message.thy Wed Sep 20 15:11:46 2006 +0200
1.3 @@ -941,8 +941,7 @@
1.4 "X \<in> synth (analz H) ==> parts{X} \<subseteq> synth (analz H) \<union> parts H";
1.5 apply (rule subset_trans)
1.6 apply (erule_tac [2] Fake_parts_insert)
1.7 -apply (rule parts_mono)
1.8 -apply (blast intro: elim:);
1.9 +apply (rule parts_mono, blast)
1.10 done
1.11
1.12 lemmas Fake_parts_sing_imp_Un = Fake_parts_sing [THEN [2] rev_subsetD]