1.1 --- a/src/HOL/Auth/NS_Public_Bad.thy	Thu Apr 24 10:33:17 2014 +0200
     1.2 +++ b/src/HOL/Auth/NS_Public_Bad.thy	Thu Apr 24 17:52:19 2014 +0200
     1.3 @@ -44,8 +44,7 @@
     1.4  
     1.5  declare knows_Spy_partsEs [elim]
     1.6  declare analz_into_parts [dest]
     1.7 -declare Fake_parts_insert_in_Un  [dest]
     1.8 -declare image_eq_UN [simp]  (*accelerates proofs involving nested images*)
     1.9 +declare Fake_parts_insert_in_Un [dest]
    1.10  
    1.11  (*A "possibility property": there are traces that reach the end*)
    1.12  lemma "\<exists>NB. \<exists>evs \<in> ns_public. Says A B (Crypt (pubEK B) (Nonce NB)) \<in> set evs"