# HG changeset patch
# User wenzelm
# Date 964715144 -7200
# Node ID 4b37161f2b2ed907e79b62170fa2cc66e1bee3b0
# Parent  fc02c5bacaab9e7cdc670730a313f6708e4c5bd0
added enter_forward_proof;

diff -r fc02c5bacaab -r 4b37161f2b2e src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Thu Jul 27 18:25:28 2000 +0200
+++ b/src/Pure/Isar/toplevel.ML	Thu Jul 27 18:25:44 2000 +0200
@@ -26,6 +26,7 @@
   val sign_of: state -> Sign.sg
   val context_of: state -> Proof.context
   val proof_of: state -> Proof.state
+  val enter_forward_proof: state -> Proof.state
   type transition
   exception TERMINATE
   exception RESTART
@@ -151,6 +152,7 @@
 val sign_of = Theory.sign_of o theory_of;
 val proof_of = node_case (fn _ => raise UNDEF) I;
 
+val enter_forward_proof = node_case Proof.init_state Proof.enter_forward;
 
 
 (** toplevel transitions **)