clarified signature -- better support for Isar commands outside of Pure;
authorwenzelm
Fri, 05 Jun 2015 11:11:26 +0200
changeset 60369 f393a3fe884c
parent 60368 d3f561aa2af6
child 60370 9ec1d3d2068e
clarified signature -- better support for Isar commands outside of Pure;
src/Pure/Isar/proof.ML
--- 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