equal
deleted
inserted
replaced
538 method_setup valid_certificate_tac = {* |
538 method_setup valid_certificate_tac = {* |
539 Args.goal_spec >> (fn quant => fn ctxt => SIMPLE_METHOD'' quant |
539 Args.goal_spec >> (fn quant => fn ctxt => SIMPLE_METHOD'' quant |
540 (fn i => |
540 (fn i => |
541 EVERY [forward_tac ctxt @{thms Gets_certificate_valid} i, |
541 EVERY [forward_tac ctxt @{thms Gets_certificate_valid} i, |
542 assume_tac ctxt i, |
542 assume_tac ctxt i, |
543 etac conjE i, REPEAT (hyp_subst_tac ctxt i)])) |
543 eresolve_tac ctxt [conjE] i, REPEAT (hyp_subst_tac ctxt i)])) |
544 *} |
544 *} |
545 |
545 |
546 text{*The @{text "(no_asm)"} attribute is essential, since it retains |
546 text{*The @{text "(no_asm)"} attribute is essential, since it retains |
547 the quantifier and allows the simprule's condition to itself be simplified.*} |
547 the quantifier and allows the simprule's condition to itself be simplified.*} |
548 lemma symKey_compromise [rule_format (no_asm)]: |
548 lemma symKey_compromise [rule_format (no_asm)]: |