src/HOL/Auth/NS_Shared.thy
changeset 56681 e8d5d60d655e
parent 55417 01fbfb60c33e
child 58860 fee7cfa69c50
     1.1 --- a/src/HOL/Auth/NS_Shared.thy	Thu Apr 24 10:33:17 2014 +0200
     1.2 +++ b/src/HOL/Auth/NS_Shared.thy	Thu Apr 24 17:52:19 2014 +0200
     1.3 @@ -86,7 +86,6 @@
     1.4  declare parts.Body  [dest]
     1.5  declare Fake_parts_insert_in_Un  [dest]
     1.6  declare analz_into_parts [dest]
     1.7 -declare image_eq_UN [simp]  (*accelerates proofs involving nested images*)
     1.8  
     1.9  
    1.10  text{*A "possibility property": there are traces that reach the end*}