src/HOL/Real/Real.thy
changeset 7077 60b098bb8b8a
parent 5588 a3ab526bb891
child 7219 4e3f386c2e37
     1.1 --- a/src/HOL/Real/Real.thy	Fri Jul 23 17:28:18 1999 +0200
     1.2 +++ b/src/HOL/Real/Real.thy	Fri Jul 23 17:29:12 1999 +0200
     1.3 @@ -1,9 +1,8 @@
     1.4 -(*  Title:      Real/Real.thy
     1.5 -    ID:         $Id$
     1.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 -    Copyright   1998  University of Cambridge
     1.8 -
     1.9 -Type "real" is a linear order
    1.10 +(*  Title:       Real/Real.thy
    1.11 +    Author:      Lawrence C. Paulson
    1.12 +                 Jacques D. Fleuriot
    1.13 +    Copyright:   1998  University of Cambridge
    1.14 +    Description: Type "real" is a linear order
    1.15  *)
    1.16  
    1.17  Real = RealDef +