# HG changeset patch
# User haftmann
# Date 1248781060 -7200
# Node ID fa8872f21ac3d58b1e94d2018115851f4733a6ba
# Parent  0be31453f698495cc0d5c9904b3ced8498ed86fc
reinserted legacy ML function

diff -r 0be31453f698 -r fa8872f21ac3 doc-src/TutorialI/Protocol/Message.thy
--- 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'