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