author | wenzelm |
Thu, 31 May 2007 13:00:56 +0200 | |
changeset 23148 | ef3fa1386102 |
parent 21590 | ef7278f553eb |
child 23916 | 0f8ad1044527 |
permissions | -rw-r--r-- |
13957 | 1 |
(* Title: HOL/Complex/ROOT.ML |
2 |
ID: $Id$ |
|
3 |
Author: Jacques Fleuriot |
|
4 |
||
21590 | 5 |
The Complex Numbers. |
13957 | 6 |
*) |
7 |
||
20809 | 8 |
no_document use_thy "Infinite_Set"; |
21256 | 9 |
no_document use_thy "Parity"; |
10 |
||
11 |
with_path "../Real" use_thy "Float"; |
|
13957 | 12 |
with_path "../Hyperreal" use_thy "Hyperreal"; |
21590 | 13 |
use_thy "Complex_Main"; |