equal
deleted
inserted
replaced
126 ==> K \<in> parts (knows Spy evs)" |
126 ==> K \<in> parts (knows Spy evs)" |
127 by blast |
127 by blast |
128 |
128 |
129 text{*Forwarding lemma: see comments in OtwayRees.thy*} |
129 text{*Forwarding lemma: see comments in OtwayRees.thy*} |
130 lemmas OR2_parts_knows_Spy = |
130 lemmas OR2_parts_knows_Spy = |
131 OR2_analz_knows_Spy [THEN analz_into_parts, standard] |
131 OR2_analz_knows_Spy [THEN analz_into_parts] |
132 |
132 |
133 |
133 |
134 text{*Theorems of the form @{term "X \<notin> parts (spies evs)"} imply that |
134 text{*Theorems of the form @{term "X \<notin> parts (spies evs)"} imply that |
135 NOBODY sends messages containing X! *} |
135 NOBODY sends messages containing X! *} |
136 |
136 |