changeset 30549 | d2d7874648bd |
parent 30510 | 4120fc59dd85 |
child 32960 | 69916a850301 |
--- a/src/HOL/SET-Protocol/EventSET.thy Mon Mar 16 17:51:24 2009 +0100 +++ b/src/HOL/SET-Protocol/EventSET.thy Mon Mar 16 18:24:30 2009 +0100 @@ -189,7 +189,7 @@ *} method_setup analz_mono_contra = {* - Method.no_args (SIMPLE_METHOD (REPEAT_FIRST analz_mono_contra_tac)) *} + Scan.succeed (K (SIMPLE_METHOD (REPEAT_FIRST analz_mono_contra_tac))) *} "for proving theorems of the form X \<notin> analz (knows Spy evs) --> P" end