src/HOL/Auth/Shared.ML
changeset 6334 e53457213857
parent 6308 76f3865a2b1d
child 6915 4ab8e31a8421
equal deleted inserted replaced
6333:b1dec44d0018 6334:e53457213857
    61 (*Prove that the agent is uncompromised by the confidentiality of 
    61 (*Prove that the agent is uncompromised by the confidentiality of 
    62   a component of a message she's said.*)
    62   a component of a message she's said.*)
    63 fun not_bad_tac s =
    63 fun not_bad_tac s =
    64     case_tac ("(" ^ s ^ ") : bad") THEN'
    64     case_tac ("(" ^ s ^ ") : bad") THEN'
    65     SELECT_GOAL 
    65     SELECT_GOAL 
    66       (REPEAT_DETERM (dtac (Says_imp_spies RS analz.Inj) 1) THEN
    66       (REPEAT_DETERM (etac exE 1) THEN
       
    67        REPEAT_DETERM (dtac (Says_imp_spies RS analz.Inj) 1) THEN
    67        REPEAT_DETERM (etac MPair_analz 1) THEN
    68        REPEAT_DETERM (etac MPair_analz 1) THEN
    68        THEN_BEST_FIRST 
    69        THEN_BEST_FIRST 
    69          (dres_inst_tac [("A", s)] Crypt_Spy_analz_bad 1 THEN assume_tac 1)
    70          (dres_inst_tac [("A", s)] Crypt_Spy_analz_bad 1 THEN assume_tac 1)
    70          (has_fewer_prems 1, size_of_thm)
    71          (has_fewer_prems 1, size_of_thm)
    71          (Step_tac 1));
    72          (Step_tac 1));