# HG changeset patch
# User wenzelm
# Date 1433495486 -7200
# Node ID f393a3fe884ca926783df7f9133ba3e4349c773a
# Parent  d3f561aa2af654f92913faea349cb47ee14ee760
clarified signature -- better support for Isar commands outside of Pure;

diff -r d3f561aa2af6 -r f393a3fe884c 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