author | haftmann |
Tue, 04 Oct 2005 10:58:46 +0200 | |
changeset 17749 | 4fb42f4d61df |
parent 16784 | 92ff7c903585 |
child 20809 | 6c4fd0b4b63a |
permissions | -rw-r--r-- |
13957 | 1 |
(* Title: HOL/Complex/ROOT.ML |
2 |
ID: $Id$ |
|
3 |
Author: Jacques Fleuriot |
|
4 |
||
5 |
The Complex Numbers |
|
6 |
*) |
|
7 |
||
16784 | 8 |
with_path "../Real" use_thy "Float"; |
13957 | 9 |
with_path "../Hyperreal" use_thy "Hyperreal"; |
13984
e055ba9020eb
new theory Complex_Main as basis for analysis developments
paulson
parents:
13966
diff
changeset
|
10 |
time_use_thy "Complex_Main"; |