author | paulson |
Thu, 07 Nov 1996 10:15:57 +0100 | |
changeset 2165 | 63dfe7f19cad |
parent 2164 | c87368fc736b |
child 2166 | d276a806cc10 |
--- a/src/HOL/Auth/NS_Shared.ML Thu Nov 07 10:11:06 1996 +0100 +++ b/src/HOL/Auth/NS_Shared.ML Thu Nov 07 10:15:57 1996 +0100 @@ -288,7 +288,6 @@ (!simpset addsimps ([insert_Key_singleton, insert_Key_image, pushKey_newK] @ pushes) setloop split_tac [expand_if]))); -(** LEVEL 6 **) (*NS3, Fake*) by (EVERY (map spy_analz_tac [5,2])); by (REPEAT (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1));