src/HOL/Auth/Message.thy
changeset 18492 b0fe60800623
parent 17729 d74d0b5052a0
child 20648 742c30fc3fcb
     1.1 --- a/src/HOL/Auth/Message.thy	Thu Dec 22 13:31:58 2005 +0100
     1.2 +++ b/src/HOL/Auth/Message.thy	Thu Dec 22 14:22:11 2005 +0100
     1.3 @@ -252,8 +252,9 @@
     1.4  
     1.5  text{*Cut*}
     1.6  lemma parts_cut:
     1.7 -     "[| Y\<in> parts (insert X G);  X\<in> parts H |] ==> Y\<in> parts (G \<union> H)"
     1.8 -by (erule parts_trans, auto)
     1.9 +     "[| Y\<in> parts (insert X G);  X\<in> parts H |] ==> Y\<in> parts (G \<union> H)" 
    1.10 +by (blast intro: parts_trans) 
    1.11 +
    1.12  
    1.13  lemma parts_cut_eq [simp]: "X\<in> parts H ==> parts (insert X H) = parts H"
    1.14  by (force dest!: parts_cut intro: parts_insertI)