src/HOL/Auth/Message.thy
changeset 11264 a47a9288f3f6
parent 11251 a6816d47f41d
child 11270 a315a3862bb4
     1.1 --- a/src/HOL/Auth/Message.thy	Mon Apr 23 17:11:19 2001 +0200
     1.2 +++ b/src/HOL/Auth/Message.thy	Tue Apr 24 12:19:01 2001 +0200
     1.3 @@ -146,4 +146,12 @@
     1.4      Method.no_args (Method.METHOD (fn facts => spy_analz_tac 1)) *}
     1.5      "for proving the Fake case when analz is involved"
     1.6  
     1.7 +method_setup atomic_spy_analz = {*
     1.8 +    Method.no_args (Method.METHOD (fn facts => atomic_spy_analz_tac 1)) *}
     1.9 +    "for debugging spy_analz"
    1.10 +
    1.11 +method_setup Fake_insert_simp = {*
    1.12 +    Method.no_args (Method.METHOD (fn facts => Fake_insert_simp_tac 1)) *}
    1.13 +    "for debugging spy_analz"
    1.14 +
    1.15  end