src/HOL/MetisExamples/Message.thy
changeset 25457 ba2bcae7aafd
parent 24759 b448f94b1c88
child 25710 4cdf7de81e1b
     1.1 --- a/src/HOL/MetisExamples/Message.thy	Thu Nov 22 14:51:34 2007 +0100
     1.2 +++ b/src/HOL/MetisExamples/Message.thy	Fri Nov 23 17:37:56 2007 +0100
     1.3 @@ -253,7 +253,7 @@
     1.4  
     1.5  ML{*ResAtp.problem_name := "Message__parts_cut"*}
     1.6  lemma parts_cut: "[|Y\<in> parts(insert X G);  X\<in> parts H|] ==> Y\<in> parts(G \<union> H)"
     1.7 -by (metis Un_subset_iff Un_upper1 Un_upper2 insert_subset parts_Un parts_increasing parts_trans) 
     1.8 +by (metis Un_subset_iff insert_subset parts_increasing parts_trans) 
     1.9  
    1.10  
    1.11