changeset 20809 | 6c4fd0b4b63a |
parent 16784 | 92ff7c903585 |
child 21256 | 47195501ecf7 |
20808:96d413f78870 | 20809:6c4fd0b4b63a |
---|---|
3 Author: Jacques Fleuriot |
3 Author: Jacques Fleuriot |
4 |
4 |
5 The Complex Numbers |
5 The Complex Numbers |
6 *) |
6 *) |
7 |
7 |
8 no_document use_thy "Infinite_Set"; |
|
8 with_path "../Real" use_thy "Float"; |
9 with_path "../Real" use_thy "Float"; |
9 with_path "../Hyperreal" use_thy "Hyperreal"; |
10 with_path "../Hyperreal" use_thy "Hyperreal"; |
10 time_use_thy "Complex_Main"; |
11 time_use_thy "Complex_Main"; |