src/HOL/Auth/Event.thy
changeset 59498 50b60f501b05
parent 58963 26bf09b95dda
child 60754 02924903a6fd
     1.1 --- a/src/HOL/Auth/Event.thy	Tue Feb 10 14:29:36 2015 +0100
     1.2 +++ b/src/HOL/Auth/Event.thy	Tue Feb 10 14:48:26 2015 +0100
     1.3 @@ -272,7 +272,7 @@
     1.4  {*
     1.5  fun analz_mono_contra_tac ctxt = 
     1.6    rtac @{thm analz_impI} THEN' 
     1.7 -  REPEAT1 o (dresolve_tac @{thms analz_mono_contra})
     1.8 +  REPEAT1 o (dresolve_tac ctxt @{thms analz_mono_contra})
     1.9    THEN' (mp_tac ctxt)
    1.10  *}
    1.11  
    1.12 @@ -289,7 +289,7 @@
    1.13  fun synth_analz_mono_contra_tac ctxt = 
    1.14    rtac @{thm syan_impI} THEN'
    1.15    REPEAT1 o 
    1.16 -    (dresolve_tac 
    1.17 +    (dresolve_tac ctxt
    1.18       [@{thm knows_Spy_subset_knows_Spy_Says} RS @{thm synth_analz_mono} RS @{thm contra_subsetD},
    1.19        @{thm knows_Spy_subset_knows_Spy_Notes} RS @{thm synth_analz_mono} RS @{thm contra_subsetD},
    1.20        @{thm knows_Spy_subset_knows_Spy_Gets} RS @{thm synth_analz_mono} RS @{thm contra_subsetD}])