changeset 69597 | ff784d5a5bfb |
parent 67613 | ce654b0e6d69 |
child 76287 | cdc14f94c754 |
--- a/src/HOL/Auth/OtwayReesBella.thy Sat Jan 05 17:00:43 2019 +0100 +++ b/src/HOL/Auth/OtwayReesBella.thy Sat Jan 05 17:24:33 2019 +0100 @@ -239,7 +239,7 @@ val analz_image_freshK_ss = simpset_of - (@{context} delsimps [image_insert, image_Un] + (\<^context> delsimps [image_insert, image_Un] delsimps [@{thm imp_disjL}] (*reduces blow-up*) addsimps @{thms analz_image_freshK_simps})