src/HOL/ROOT.ML
changeset 29447 a5d0c3cf305f
parent 29304 5c71a6da989d
child 29638 1f8f3d26a2cf
     1.1 --- a/src/HOL/ROOT.ML	Sun Jan 11 16:56:59 2009 +0100
     1.2 +++ b/src/HOL/ROOT.ML	Sun Jan 11 17:34:02 2009 +0100
     1.3 @@ -1,5 +1,6 @@
     1.4  (* Classical Higher-order Logic -- batteries included *)
     1.5  
     1.6 +use_thy "Main";
     1.7  use_thy "Complex_Main";
     1.8  
     1.9  val HOL_proofs = ! Proofterm.proofs;