# HG changeset patch
# User haftmann
# Date 1398511544 -7200
# Node ID 0d56854096baff53cfec63f5c702e263e64e9ef6
# Parent  13b0fc4ece4240147c56688d13cc57929353c652
avoid non-standard simp default rule

diff -r 13b0fc4ece42 -r 0d56854096ba src/Doc/Tutorial/Protocol/NS_Public.thy
--- a/src/Doc/Tutorial/Protocol/NS_Public.thy	Sat Apr 26 21:37:09 2014 +1000
+++ b/src/Doc/Tutorial/Protocol/NS_Public.thy	Sat Apr 26 13:25:44 2014 +0200
@@ -92,7 +92,6 @@
 declare knows_Spy_partsEs [elim]
 declare analz_subset_parts [THEN subsetD, dest]
 declare Fake_parts_insert [THEN subsetD, dest]
-declare image_eq_UN [simp]  (*accelerates proofs involving nested images*)
 
 (*A "possibility property": there are traces that reach the end*)
 lemma "\<exists>NB. \<exists>evs \<in> ns_public. Says A B (Crypt (pubK B) (Nonce NB)) \<in> set evs"