equal
deleted
inserted
replaced
260 delsimps [imp_disjL] (*reduces blow-up*) |
260 delsimps [imp_disjL] (*reduces blow-up*) |
261 addsimps thms "analz_image_freshK_simps" |
261 addsimps thms "analz_image_freshK_simps" |
262 *} |
262 *} |
263 |
263 |
264 method_setup analz_freshCryptK = {* |
264 method_setup analz_freshCryptK = {* |
265 Method.no_args |
265 Method.ctxt_args (fn ctxt => |
266 (Method.METHOD |
266 (Method.METHOD |
267 (fn facts => EVERY [REPEAT_FIRST (resolve_tac [allI, ballI, impI]), |
267 (fn facts => EVERY [REPEAT_FIRST (resolve_tac [allI, ballI, impI]), |
268 REPEAT_FIRST (rtac analz_image_freshCryptK_lemma), |
268 REPEAT_FIRST (rtac analz_image_freshCryptK_lemma), |
269 ALLGOALS (asm_simp_tac analz_image_freshK_ss)])) *} |
269 ALLGOALS (asm_simp_tac (Simplifier.context ctxt analz_image_freshK_ss))]))) *} |
270 "for proving useful rewrite rule" |
270 "for proving useful rewrite rule" |
271 |
271 |
272 |
272 |
273 method_setup disentangle = {* |
273 method_setup disentangle = {* |
274 Method.no_args |
274 Method.no_args |