src/HOL/ROOT.ML
changeset 29304 5c71a6da989d
parent 29249 4dc278c8dc59
child 29447 a5d0c3cf305f
     1.1 --- a/src/HOL/ROOT.ML	Thu Jan 01 23:31:59 2009 +0100
     1.2 +++ b/src/HOL/ROOT.ML	Fri Jan 02 00:21:59 2009 +0100
     1.3 @@ -1,9 +1,5 @@
     1.4 -(*  Title:      HOL/ROOT.ML
     1.5 - 
     1.6 -Classical Higher-order Logic -- batteries included.
     1.7 -*)
     1.8 +(* Classical Higher-order Logic -- batteries included *)
     1.9  
    1.10  use_thy "Complex_Main";
    1.11  
    1.12  val HOL_proofs = ! Proofterm.proofs;
    1.13 -