| changeset 17689 | a04b5b43625e |
| parent 16417 | 9bc16273c2d4 |
| child 18557 | 60a0f9caa0a2 |
--- a/src/HOL/Auth/Guard/Extensions.thy Wed Sep 28 11:14:26 2005 +0200 +++ b/src/HOL/Auth/Guard/Extensions.thy Wed Sep 28 11:15:33 2005 +0200 @@ -151,7 +151,8 @@ by (rule parts_insert_substI, simp) lemma parts_parts: "[| X:parts {Y}; Y:parts G |] ==> X:parts G" -by (drule_tac x=Y in in_sub, drule parts_mono, auto) +by (frule parts_cut, auto) + lemma parts_parts_parts: "[| X:parts {Y}; Y:parts {Z}; Z:parts G |] ==> X:parts G" by (auto dest: parts_parts)