src/Pure/Isar/proof.ML
changeset 8206 e50a130ec9af
parent 8186 61ec7bedc717
child 8234 36a85a6c4852
     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 *)