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