src/HOL/ROOT.ML
author wenzelm
Wed, 17 Sep 2008 21:27:14 +0200
changeset 28263 69eaa97e7e96
parent 27421 7e458bd56860
child 28952 15a4b2cf8c34
permissions -rw-r--r--
moved global ML bindings to global place;

(*  Title:      HOL/ROOT.ML
    ID:         $Id$
 
Classical Higher-order Logic -- batteries included.
*)

use_thy "Complex/Complex_Main";

val HOL_proofs = ! Proofterm.proofs;