(* Title: HOL/Complex/ROOT.ML ID: $Id$ Author: Jacques Fleuriot The Complex Numbers *) no_document time_use_thy "Ring_and_Field"; with_path "../Real" use_thy "Real"; with_path "../Hyperreal" use_thy "Hyperreal"; time_use_thy "Complex_Main";