# HG changeset patch
# User wenzelm
# Date 949945240 -3600
# Node ID e50a130ec9af00eee3d4e42ca4bee234b1d8e492
# Parent  9f0ff98f37f6e6c9fd3d8c1a0ee7d0931943f4bc
assert_no_chain;

diff -r 9f0ff98f37f6 -r e50a130ec9af src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Mon Feb 07 18:40:27 2000 +0100
+++ b/src/Pure/Isar/proof.ML	Mon Feb 07 18:40:40 2000 +0100
@@ -31,6 +31,7 @@
   val reset_facts: state -> state
   val assert_forward: state -> state
   val assert_backward: state -> state
+  val assert_no_chain: state -> state
   val enter_forward: state -> state
   val show_hyps: bool ref
   val pretty_thm: thm -> Pretty.T
@@ -269,6 +270,7 @@
 val assert_forward = assert_mode (equal Forward);
 val assert_forward_or_chain = assert_mode (equal Forward orf equal ForwardChain);
 val assert_backward = assert_mode (equal Backward);
+val assert_no_chain = assert_mode (not_equal ForwardChain);
 
 
 (* blocks *)