src/HOL/Auth/Message.thy
changeset 51702 dcfab8e87621
parent 45605 a89b4bc311a5
child 51717 9e7d1c139569
--- a/src/HOL/Auth/Message.thy	Fri Apr 12 15:30:38 2013 +0200
+++ b/src/HOL/Auth/Message.thy	Fri Apr 12 17:02:55 2013 +0200
@@ -851,7 +851,6 @@
 {*
 (*Analysis of Fake cases.  Also works for messages that forward unknown parts,
   but this application is no longer necessary if analz_insert_eq is used.
-  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})