changeset 32265 | fa8872f21ac3 |
parent 32149 | ef59550a55d3 |
child 32960 | 69916a850301 |
--- a/doc-src/TutorialI/Protocol/Message.thy Tue Jul 28 13:37:09 2009 +0200 +++ b/doc-src/TutorialI/Protocol/Message.thy Tue Jul 28 13:37:40 2009 +0200 @@ -841,6 +841,8 @@ (*Apply rules to break down assumptions of the form Y \<in> parts(insert X H) and Y \<in> analz(insert X H) *) +fun impOfSubs th = th RSN (2, @{thm rev_subsetD}) + val Fake_insert_tac = dresolve_tac [impOfSubs Fake_analz_insert, impOfSubs Fake_parts_insert] THEN'