assert_no_chain;
authorwenzelm
Mon Feb 07 18:40:40 2000 +0100 (2000-02-07)
changeset 8206e50a130ec9af
parent 8205 9f0ff98f37f6
child 8207 985c876b777e
assert_no_chain;
src/Pure/Isar/proof.ML
     1.1 --- a/src/Pure/Isar/proof.ML	Mon Feb 07 18:40:27 2000 +0100
     1.2 +++ b/src/Pure/Isar/proof.ML	Mon Feb 07 18:40:40 2000 +0100
     1.3 @@ -31,6 +31,7 @@
     1.4    val reset_facts: state -> state
     1.5    val assert_forward: state -> state
     1.6    val assert_backward: state -> state
     1.7 +  val assert_no_chain: state -> state
     1.8    val enter_forward: state -> state
     1.9    val show_hyps: bool ref
    1.10    val pretty_thm: thm -> Pretty.T
    1.11 @@ -269,6 +270,7 @@
    1.12  val assert_forward = assert_mode (equal Forward);
    1.13  val assert_forward_or_chain = assert_mode (equal Forward orf equal ForwardChain);
    1.14  val assert_backward = assert_mode (equal Backward);
    1.15 +val assert_no_chain = assert_mode (not_equal ForwardChain);
    1.16  
    1.17  
    1.18  (* blocks *)