equal
deleted
inserted
replaced
374 ALLGOALS (clarify_tac ctxt), |
374 ALLGOALS (clarify_tac ctxt), |
375 ALLGOALS (asm_lr_simp_tac ss)]) |
375 ALLGOALS (asm_lr_simp_tac ss)]) |
376 end; |
376 end; |
377 *} |
377 *} |
378 |
378 |
379 method_setup ensures_tac = {* |
379 method_setup ensures = {* |
380 Args.goal_spec -- Scan.lift Args.name_source >> |
380 Args.goal_spec -- Scan.lift Args.name_source >> |
381 (fn (quant, s) => fn ctxt => SIMPLE_METHOD'' quant (ensures_tac ctxt s)) |
381 (fn (quant, s) => fn ctxt => SIMPLE_METHOD'' quant (ensures_tac ctxt s)) |
382 *} "for proving progress properties" |
382 *} "for proving progress properties" |
383 |
383 |
384 end |
384 end |