src/Pure/Isar/proof.ML
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