author | wenzelm |
Fri, 05 Jun 2015 11:11:26 +0200 | |
changeset 60369 | f393a3fe884c |
parent 60368 | d3f561aa2af6 |
child 60370 | 9ec1d3d2068e |
--- a/src/Pure/Isar/proof.ML Wed Jun 03 21:48:40 2015 +0200 +++ b/src/Pure/Isar/proof.ML Fri Jun 05 11:11:26 2015 +0200 @@ -31,6 +31,8 @@ val assert_backward: state -> state val assert_no_chain: state -> state val enter_forward: state -> state + val enter_chain: state -> state + val enter_backward: state -> state val has_bottom_goal: state -> bool val pretty_state: int -> state -> Pretty.T list val refine: Method.text -> state -> state Seq.seq