src/HOL/ROOT.ML
author wenzelm
Wed Sep 17 21:27:14 2008 +0200 (2008-09-17)
changeset 28263 69eaa97e7e96
parent 27421 7e458bd56860
child 28952 15a4b2cf8c34
permissions -rw-r--r--
moved global ML bindings to global place;
clasohm@1264
     1
(*  Title:      HOL/ROOT.ML
clasohm@923
     2
    ID:         $Id$
wenzelm@23166
     3
 
haftmann@27368
     4
Classical Higher-order Logic -- batteries included.
clasohm@923
     5
*)
clasohm@923
     6
haftmann@27421
     7
use_thy "Complex/Complex_Main";
wenzelm@28263
     8
wenzelm@28263
     9
val HOL_proofs = ! Proofterm.proofs;
wenzelm@28263
    10