src/Pure/Isar/proof.ML

   val goal_facts: (state -> thm list) -> state -> state
   val use_facts: state -> state
   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
   val pretty_thms: thm list -> Pretty.T
   val verbose: bool ref

 
 fun is_chain state = get_mode state = ForwardChain;
 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 *)
 
 fun level (State (_, nodes)) = length nodes;