# HG changeset patch
# User webertj
# Date 1154103082 -7200
# Node ID 54db3583354f50171c791723ec86bb770ea9eb0c
# Parent  89a407400874bc947989502707922d155df7414c
title fixed

diff -r 89a407400874 -r 54db3583354f src/HOL/Hyperreal/HyperDef.thy
--- a/src/HOL/Hyperreal/HyperDef.thy	Thu Jul 27 23:28:30 2006 +0200
+++ b/src/HOL/Hyperreal/HyperDef.thy	Fri Jul 28 18:11:22 2006 +0200
@@ -1,4 +1,4 @@
-(*  Title       : HOL/Real/Hyperreal/HyperDef.thy
+(*  Title       : HOL/Hyperreal/HyperDef.thy
     ID          : $Id$
     Author      : Jacques D. Fleuriot
     Copyright   : 1998  University of Cambridge
diff -r 89a407400874 -r 54db3583354f src/HOL/Hyperreal/fuf.ML
--- a/src/HOL/Hyperreal/fuf.ML	Thu Jul 27 23:28:30 2006 +0200
+++ b/src/HOL/Hyperreal/fuf.ML	Fri Jul 28 18:11:22 2006 +0200
@@ -1,4 +1,4 @@
-(*  Title       : HOL/Real/Hyperreal/fuf.ML
+(*  Title       : HOL/Hyperreal/fuf.ML
     ID          : $Id$
     Author      : Jacques D. Fleuriot
     Copyright   : 1998  University of Cambridge