src/HOL/Complex/ROOT.ML
author huffman
Tue, 01 Jul 2008 03:14:00 +0200
changeset 27416 07e04ab0177a
parent 27298 a5373b60e66c
permissions -rw-r--r--
remove unused lemmas ub2ub_monofun' and dir2dir_monofun

(*  Title:      HOL/Complex/ROOT.ML
    ID:         $Id$
    Author:     Jacques Fleuriot

The Complex Numbers.
*)

use_thy "Complex_Main";