equal
deleted
inserted
replaced
849 subsection{*Tactics useful for many protocol proofs*} |
849 subsection{*Tactics useful for many protocol proofs*} |
850 ML |
850 ML |
851 {* |
851 {* |
852 (*Analysis of Fake cases. Also works for messages that forward unknown parts, |
852 (*Analysis of Fake cases. Also works for messages that forward unknown parts, |
853 but this application is no longer necessary if analz_insert_eq is used. |
853 but this application is no longer necessary if analz_insert_eq is used. |
854 Abstraction over i is ESSENTIAL: it delays the dereferencing of claset |
|
855 DEPENDS UPON "X" REFERRING TO THE FRADULENT MESSAGE *) |
854 DEPENDS UPON "X" REFERRING TO THE FRADULENT MESSAGE *) |
856 |
855 |
857 fun impOfSubs th = th RSN (2, @{thm rev_subsetD}) |
856 fun impOfSubs th = th RSN (2, @{thm rev_subsetD}) |
858 |
857 |
859 (*Apply rules to break down assumptions of the form |
858 (*Apply rules to break down assumptions of the form |