| changeset 44174 | d1d79f0e1ea6 |
| parent 43582 | ddca453102ab |
| child 45605 | a89b4bc311a5 |
--- a/src/HOL/Auth/Message.thy Fri Aug 12 09:17:30 2011 -0700 +++ b/src/HOL/Auth/Message.thy Fri Aug 12 14:45:50 2011 -0700 @@ -841,7 +841,7 @@ apply (erule analz.induct, auto) apply (blast dest:parts.Body) apply (blast dest: parts.Body) -apply (metis Un_absorb2 keyfree_KeyE mem_def parts_Un parts_keyfree sup1I2) +apply (metis Un_absorb2 keyfree_KeyE parts_Un parts_keyfree UnI2) done subsection{*Tactics useful for many protocol proofs*}