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