author | ballarin |
Mon, 02 Aug 2004 10:12:02 +0200 | |
changeset 15096 | be1d3b8cfbd5 |
parent 14334 | 6137d24eef79 |
child 16784 | 92ff7c903585 |
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 |
||
14334 | 8 |
with_path "../Real" use_thy "Real"; |
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"; |