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