src/HOL/ROOT.ML
changeset 33113 0f6e30b87cf1
parent 30126 332e739b6b0e
     1.1 --- a/src/HOL/ROOT.ML	Sat Oct 24 16:55:42 2009 +0200
     1.2 +++ b/src/HOL/ROOT.ML	Sat Oct 24 16:55:42 2009 +0200
     1.3 @@ -1,5 +1,6 @@
     1.4  (* Classical Higher-order Logic -- batteries included *)
     1.5  
     1.6 +Toplevel.debug := true;
     1.7  use_thy "Complex_Main";
     1.8  
     1.9  val HOL_proofs = ! Proofterm.proofs;