src/HOL/Auth/Event.thy
changeset 60754 02924903a6fd
parent 59498 50b60f501b05
child 61830 4f5ab843cf5b
     1.1 --- a/src/HOL/Auth/Event.thy	Sat Jul 18 20:53:05 2015 +0200
     1.2 +++ b/src/HOL/Auth/Event.thy	Sat Jul 18 20:54:56 2015 +0200
     1.3 @@ -271,7 +271,7 @@
     1.4  ML
     1.5  {*
     1.6  fun analz_mono_contra_tac ctxt = 
     1.7 -  rtac @{thm analz_impI} THEN' 
     1.8 +  resolve_tac ctxt @{thms analz_impI} THEN' 
     1.9    REPEAT1 o (dresolve_tac ctxt @{thms analz_mono_contra})
    1.10    THEN' (mp_tac ctxt)
    1.11  *}
    1.12 @@ -287,7 +287,7 @@
    1.13  ML
    1.14  {*
    1.15  fun synth_analz_mono_contra_tac ctxt = 
    1.16 -  rtac @{thm syan_impI} THEN'
    1.17 +  resolve_tac ctxt @{thms syan_impI} THEN'
    1.18    REPEAT1 o 
    1.19      (dresolve_tac ctxt
    1.20       [@{thm knows_Spy_subset_knows_Spy_Says} RS @{thm synth_analz_mono} RS @{thm contra_subsetD},