# 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 "\NB. \evs \ ns_public. Says A B (Crypt (pubK B) (Nonce NB)) \ set evs"