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