full_proofs;
authorwenzelm
Mon, 21 Jan 2002 22:27:34 +0100
changeset 12833 9f3226cfe021
parent 12832 c31b44286a8a
child 12834 e5bec3268932
full_proofs;
src/Pure/proof_general.ML
--- 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