title fixed
authorwebertj
Fri, 28 Jul 2006 18:11:22 +0200
changeset 20245 54db3583354f
parent 20244 89a407400874
child 20246 fdfe7399e057
title fixed
src/HOL/Hyperreal/HyperDef.thy
src/HOL/Hyperreal/fuf.ML
--- 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
--- 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