src/HOL/Real/Real.thy
changeset 7334 a90fc1e5fb19
parent 7219 4e3f386c2e37
child 7562 8519d5019309
     1.1 --- a/src/HOL/Real/Real.thy	Tue Aug 24 11:50:58 1999 +0200
     1.2 +++ b/src/HOL/Real/Real.thy	Tue Aug 24 11:54:13 1999 +0200
     1.3 @@ -1,14 +1,2 @@
     1.4 -(*  Title:       Real/Real.thy
     1.5 -    ID          : $Id$
     1.6 -    Author:      Lawrence C. Paulson
     1.7 -                 Jacques D. Fleuriot
     1.8 -    Copyright:   1998  University of Cambridge
     1.9 -    Description: Type "real" is a linear order
    1.10 -*)
    1.11  
    1.12 -Real = RealDef +
    1.13 -
    1.14 -instance real :: order (real_le_refl,real_le_trans,real_le_anti_sym,real_less_le)
    1.15 -instance real :: linorder (real_le_linear)
    1.16 -
    1.17 -end
    1.18 +Real = RComplete