changeset 60369 | f393a3fe884c |
parent 60094 | 96a4765ba7d1 |
child 60371 | 8a5cfdda1b98 |
--- 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