# HG changeset patch
# User wenzelm
# Date 1365778975 -7200
# Node ID dcfab8e876215b1e1c3fc86a61ca3981721dc25f
# Parent  1e29891759c444d264f638a086f48edb7c686c24
removed historic comments;

diff -r 1e29891759c4 -r dcfab8e87621 src/HOL/Auth/Message.thy
--- 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})
diff -r 1e29891759c4 -r dcfab8e87621 src/HOL/SET_Protocol/Message_SET.thy
--- 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})