| changeset 27882 | eaa9fef9f4c1 |
| parent 27239 | f2f42f9fa09d |
| child 30549 | d2d7874648bd |
| 27881:f0d543629376 | 27882:eaa9fef9f4c1 |
|---|---|
376 end; |
376 end; |
377 *} |
377 *} |
378 |
378 |
379 method_setup ensures_tac = {* |
379 method_setup ensures_tac = {* |
380 fn args => fn ctxt => |
380 fn args => fn ctxt => |
381 Method.goal_args' (Scan.lift Args.name) (ensures_tac ctxt) |
381 Method.goal_args' (Scan.lift Args.name_source) (ensures_tac ctxt) |
382 args ctxt *} |
382 args ctxt *} |
383 "for proving progress properties" |
383 "for proving progress properties" |
384 |
384 |
385 end |
385 end |