# HG changeset patch
# User wenzelm
# Date 1120050815 -7200
# Node ID 4590c1f790508204174cf584907a0032f15c4281
# Parent  6207f475bebb9d0e2952dd64c9dff39796689c03
added print_mode three_buffersN and corresponding cond_print;

diff -r 6207f475bebb -r 4590c1f79050 src/Pure/Isar/isar_thy.ML
--- a/src/Pure/Isar/isar_thy.ML	Wed Jun 29 15:13:34 2005 +0200
+++ b/src/Pure/Isar/isar_thy.ML	Wed Jun 29 15:13:35 2005 +0200
@@ -128,6 +128,8 @@
   val apply: Method.text -> ProofHistory.T -> ProofHistory.T
   val apply_end: Method.text -> ProofHistory.T -> ProofHistory.T
   val proof: Method.text option -> ProofHistory.T -> ProofHistory.T
+  val three_buffersN: string
+  val cond_print: Toplevel.transition -> Toplevel.transition
   val qed: Method.text option -> Toplevel.transition -> Toplevel.transition
   val terminal_proof: Method.text * Method.text option
     -> Toplevel.transition -> Toplevel.transition
@@ -459,6 +461,9 @@
 
 (* local endings *)
 
+val three_buffersN = "three_buffers";
+val cond_print = Toplevel.print' three_buffersN;
+
 val local_qed = proof'' o (ProofHistory.applys oo Method.local_qed true);
 val skip_local_qed =
   Toplevel.skip_proof (History.apply (fn i => if i > 1 then i - 1 else raise Toplevel.UNDEF));