# HG changeset patch
# User wenzelm
# Date 1011648454 -3600
# Node ID 9f3226cfe0219d7af7ce0f6dce3ba033129120c5
# Parent  c31b44286a8a6b0786abb0bb65ee5359024ea062
full_proofs;

diff -r c31b44286a8a -r 9f3226cfe021 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