--- 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 **)