HOL-Real/Complex_Numbers;
authorwenzelm
Sun Jan 13 19:45:17 2002 +0100 (2002-01-13)
changeset 12734c5f6d8259ecd
parent 12733 611ab32b2176
child 12735 09a224f7d776
HOL-Real/Complex_Numbers;
NEWS
src/HOL/Real/Real.thy
     1.1 --- a/NEWS	Sun Jan 13 19:42:30 2002 +0100
     1.2 +++ b/NEWS	Sun Jan 13 19:45:17 2002 +0100
     1.3 @@ -251,6 +251,8 @@
     1.4  parts turned into readable document, with proper Isar proof texts and
     1.5  some explanations (by Gerwin Klein);
     1.6  
     1.7 +* HOL-Real: added Complex_Numbers (by Gertrud Bauer);
     1.8 +
     1.9  * HOL-Hyperreal is now a logic image;
    1.10  
    1.11  
     2.1 --- a/src/HOL/Real/Real.thy	Sun Jan 13 19:42:30 2002 +0100
     2.2 +++ b/src/HOL/Real/Real.thy	Sun Jan 13 19:45:17 2002 +0100
     2.3 @@ -1,2 +1,2 @@
     2.4  
     2.5 -Real = RComplete + RealPow
     2.6 +Real = RComplete + Complex_Numbers