--- 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})
--- a/src/HOL/SET_Protocol/Message_SET.thy Fri Apr 12 15:30:38 2013 +0200
+++ b/src/HOL/SET_Protocol/Message_SET.thy Fri Apr 12 17:02:55 2013 +0200
@@ -841,7 +841,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})