src/Pure/proof_general.ML

   val help: unit -> unit
   val show_context: unit -> theory
   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;
 
 structure ProofGeneral: PROOF_GENERAL =

 
 fun isa_restart () = restart false;
 fun isar_restart () = (sync_thy_loader (); restart true; raise Toplevel.RESTART);
 
 end;
+
+
+fun full_proofs true = proofs := 2
+  | full_proofs false = proofs := 1;
 
 
 (* outer syntax *)
 
 local structure P = OuterParse and K = OuterSyntax.Keyword in