src/HOL/ROOT.ML
author wenzelm
Fri, 15 Aug 2008 15:50:52 +0200
changeset 27885 76b51cd0a37c
parent 27421 7e458bd56860
child 28263 69eaa97e7e96
permissions -rw-r--r--
renamed T.source_of' to T.source_position_of;

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

use_thy "Complex/Complex_Main";