updated not_bad_tac for the Gets model
authorpaulson
Wed Mar 10 10:42:40 1999 +0100 (1999-03-10)
changeset 6334e53457213857
parent 6333 b1dec44d0018
child 6335 7e4bffaa2a3e
updated not_bad_tac for the Gets model
src/HOL/Auth/Shared.ML
     1.1 --- a/src/HOL/Auth/Shared.ML	Wed Mar 10 10:42:11 1999 +0100
     1.2 +++ b/src/HOL/Auth/Shared.ML	Wed Mar 10 10:42:40 1999 +0100
     1.3 @@ -63,7 +63,8 @@
     1.4  fun not_bad_tac s =
     1.5      case_tac ("(" ^ s ^ ") : bad") THEN'
     1.6      SELECT_GOAL 
     1.7 -      (REPEAT_DETERM (dtac (Says_imp_spies RS analz.Inj) 1) THEN
     1.8 +      (REPEAT_DETERM (etac exE 1) THEN
     1.9 +       REPEAT_DETERM (dtac (Says_imp_spies RS analz.Inj) 1) THEN
    1.10         REPEAT_DETERM (etac MPair_analz 1) THEN
    1.11         THEN_BEST_FIRST 
    1.12           (dres_inst_tac [("A", s)] Crypt_Spy_analz_bad 1 THEN assume_tac 1)