src/HOL/Real/Real.thy
changeset 7219 4e3f386c2e37
parent 7077 60b098bb8b8a
child 7334 a90fc1e5fb19
     1.1 --- a/src/HOL/Real/Real.thy	Mon Aug 16 18:41:06 1999 +0200
     1.2 +++ b/src/HOL/Real/Real.thy	Mon Aug 16 18:41:32 1999 +0200
     1.3 @@ -1,4 +1,5 @@
     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