src/HOL/Complex/ROOT.ML
author paulson
Thu Jul 01 12:29:53 2004 +0200 (2004-07-01)
changeset 15013 34264f5e4691
parent 14334 6137d24eef79
child 16784 92ff7c903585
permissions -rw-r--r--
new treatment of binary numerals
paulson@13957
     1
(*  Title:      HOL/Complex/ROOT.ML
paulson@13957
     2
    ID:         $Id$
paulson@13957
     3
    Author:     Jacques Fleuriot
paulson@13957
     4
paulson@13957
     5
The Complex Numbers
paulson@13957
     6
*)
paulson@13957
     7
paulson@14334
     8
with_path "../Real"      use_thy "Real";
paulson@13957
     9
with_path "../Hyperreal" use_thy "Hyperreal";
paulson@13984
    10
time_use_thy "Complex_Main";