src/HOL/SET-Protocol/MessageSET.thy

--- a/src/HOL/SET-Protocol/MessageSET.thy	Tue Jul 21 07:55:56 2009 +0200
+++ b/src/HOL/SET-Protocol/MessageSET.thy	Tue Jul 21 11:09:50 2009 +0200
@@ -854,6 +854,8 @@
   Abstraction over i is ESSENTIAL: it delays the dereferencing of claset
   DEPENDS UPON "X" REFERRING TO THE FRADULENT MESSAGE *)
 
+fun impOfSubs th = th RSN (2, @{thm rev_subsetD})
+
 (*Apply rules to break down assumptions of the form
   Y \<in> parts(insert X H)  and  Y \<in> analz(insert X H)
 *)