equal
deleted
inserted
replaced
1 (* Title: src/HOL/Library/Extended_Reals.thy |
1 (* Title: HOL/Library/Extended_Reals.thy |
2 Author: Johannes Hölzl; TU München |
2 Author: Johannes Hölzl, TU München |
3 Author: Robert Himmelmann; TU München |
3 Author: Robert Himmelmann, TU München |
4 Author: Armin Heller; TU München |
4 Author: Armin Heller, TU München |
5 Author: Bogdan Grechuk; University of Edinburgh *) |
5 Author: Bogdan Grechuk, University of Edinburgh |
|
6 *) |
6 |
7 |
7 header {* Extended real number line *} |
8 header {* Extended real number line *} |
8 |
9 |
9 theory Extended_Reals |
10 theory Extended_Reals |
10 imports Complex_Main |
11 imports Complex_Main |