# HG changeset patch
# User wenzelm
# Date 1235678219 -3600
# Node ID 1c912a9d820067652aa148be27711d8878dc9304
# Parent  5c7bcb296600e031251cd64f243a065b106609eb
standard headers;
eliminated non-ASCII chars, which are fragile in the age of unicode;

diff -r 5c7bcb296600 -r 1c912a9d8200 src/HOL/Decision_Procs/Approximation.thy
--- a/src/HOL/Decision_Procs/Approximation.thy	Thu Feb 26 20:55:47 2009 +0100
+++ b/src/HOL/Decision_Procs/Approximation.thy	Thu Feb 26 20:56:59 2009 +0100
@@ -1,7 +1,9 @@
-(* Title:     HOL/Reflection/Approximation.thy
- * Author:    Johannes Hölzl <hoelzl@in.tum.de> 2008 / 2009
- *)
+(*  Title:      HOL/Reflection/Approximation.thy
+    Author:     Johannes Hoelzl <hoelzl@in.tum.de> 2008 / 2009
+*)
+
 header {* Prove unequations about real numbers by computation *}
+
 theory Approximation
 imports Complex_Main Float Reflection Dense_Linear_Order Efficient_Nat
 begin
diff -r 5c7bcb296600 -r 1c912a9d8200 src/HOL/Library/Float.thy
--- a/src/HOL/Library/Float.thy	Thu Feb 26 20:55:47 2009 +0100
+++ b/src/HOL/Library/Float.thy	Thu Feb 26 20:56:59 2009 +0100
@@ -1,7 +1,7 @@
-(* Title:    HOL/Library/Float.thy
- * Author:   Steven Obua 2008
- *           Johannes HÃ\<paragraph>lzl, TU Muenchen <hoelzl@in.tum.de> 2008 / 2009
- *)
+(*  Title:      HOL/Library/Float.thy
+    Author:     Steven Obua 2008
+    Author:     Johannes Hoelzl, TU Muenchen <hoelzl@in.tum.de> 2008 / 2009
+*)
 
 header {* Floating-Point Numbers *}
 
diff -r 5c7bcb296600 -r 1c912a9d8200 src/HOL/RComplete.thy
--- a/src/HOL/RComplete.thy	Thu Feb 26 20:55:47 2009 +0100
+++ b/src/HOL/RComplete.thy	Thu Feb 26 20:56:59 2009 +0100
@@ -1,8 +1,8 @@
-(*  Title       : HOL/RComplete.thy
-    Author      : Jacques D. Fleuriot, University of Edinburgh
-    Author      : Larry Paulson, University of Cambridge
-    Author      : Jeremy Avigad, Carnegie Mellon University
-    Author      : Florian Zuleger, Johannes Hoelzl, and Simon Funke, TU Muenchen
+(*  Title:      HOL/RComplete.thy
+    Author:     Jacques D. Fleuriot, University of Edinburgh
+    Author:     Larry Paulson, University of Cambridge
+    Author:     Jeremy Avigad, Carnegie Mellon University
+    Author:     Florian Zuleger, Johannes Hoelzl, and Simon Funke, TU Muenchen
 *)
 
 header {* Completeness of the Reals; Floor and Ceiling Functions *}
diff -r 5c7bcb296600 -r 1c912a9d8200 src/HOL/ex/ApproximationEx.thy
--- a/src/HOL/ex/ApproximationEx.thy	Thu Feb 26 20:55:47 2009 +0100
+++ b/src/HOL/ex/ApproximationEx.thy	Thu Feb 26 20:56:59 2009 +0100
@@ -1,6 +1,7 @@
-(* Title:    HOL/ex/ApproximationEx.thy
-   Author:   Johannes Hoelzl <hoelzl@in.tum.de> 2009
+(*  Title:      HOL/ex/ApproximationEx.thy
+    Author:     Johannes Hoelzl <hoelzl@in.tum.de> 2009
 *)
+
 theory ApproximationEx
 imports "~~/src/HOL/Reflection/Approximation"
 begin