| 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})