--- a/src/HOL/Real/RealDef.ML Mon Aug 16 18:41:06 1999 +0200
+++ b/src/HOL/Real/RealDef.ML Mon Aug 16 18:41:32 1999 +0200
@@ -1,4 +1,5 @@
(* Title : Real/RealDef.ML
+ ID : $Id$
Author : Jacques D. Fleuriot
Copyright : 1998 University of Cambridge
Description : The reals