src/HOL/Auth/Message.thy
changeset 16796 140f1e0ea846
parent 16417 9bc16273c2d4
child 16818 2b82259cc7b2
     1.1 --- a/src/HOL/Auth/Message.thy	Wed Jul 13 15:06:04 2005 +0200
     1.2 +++ b/src/HOL/Auth/Message.thy	Wed Jul 13 15:06:20 2005 +0200
     1.3 @@ -84,11 +84,11 @@
     1.4  lemma parts_mono: "G\<subseteq>H ==> parts(G) \<subseteq> parts(H)"
     1.5  apply auto
     1.6  apply (erule parts.induct) 
     1.7 -apply (auto dest: Fst Snd Body) 
     1.8 +apply (blast dest: Fst Snd Body)+
     1.9  done
    1.10  
    1.11  
    1.12 -(*Equations hold because constructors are injective; cannot prove for all f*)
    1.13 +text{*Equations hold because constructors are injective; cannot prove for all f*}
    1.14  lemma Friend_image_eq [simp]: "(Friend x \<in> Friend`A) = (x:A)"
    1.15  by auto
    1.16