--- a/src/Pure/proof_general.ML Mon Jan 21 17:03:38 2002 +0100
+++ b/src/Pure/proof_general.ML Mon Jan 21 22:27:34 2002 +0100
@@ -19,6 +19,7 @@
val kill_goal: unit -> unit
val repeat_undo: int -> unit
val isa_restart: unit -> unit
+ val full_proofs: bool -> unit
val init: bool -> unit
val write_keywords: string -> unit
end;
@@ -254,6 +255,10 @@
end;
+fun full_proofs true = proofs := 2
+ | full_proofs false = proofs := 1;
+
+
(* outer syntax *)
local structure P = OuterParse and K = OuterSyntax.Keyword in