avoid non-standard simp default rule
authorhaftmann
Sat Apr 26 13:25:44 2014 +0200 (2014-04-26)
changeset 567390d56854096ba
parent 56738 13b0fc4ece42
child 56740 5ebaa364d8ab
avoid non-standard simp default rule
src/Doc/Tutorial/Protocol/NS_Public.thy
     1.1 --- a/src/Doc/Tutorial/Protocol/NS_Public.thy	Sat Apr 26 21:37:09 2014 +1000
     1.2 +++ b/src/Doc/Tutorial/Protocol/NS_Public.thy	Sat Apr 26 13:25:44 2014 +0200
     1.3 @@ -92,7 +92,6 @@
     1.4  declare knows_Spy_partsEs [elim]
     1.5  declare analz_subset_parts [THEN subsetD, dest]
     1.6  declare Fake_parts_insert [THEN subsetD, dest]
     1.7 -declare image_eq_UN [simp]  (*accelerates proofs involving nested images*)
     1.8  
     1.9  (*A "possibility property": there are traces that reach the end*)
    1.10  lemma "\<exists>NB. \<exists>evs \<in> ns_public. Says A B (Crypt (pubK B) (Nonce NB)) \<in> set evs"