standard headers;
authorwenzelm
Thu Feb 26 20:56:59 2009 +0100 (2009-02-26)
changeset 301221c912a9d8200
parent 30121 5c7bcb296600
child 30123 25a3531c0df5
standard headers;
eliminated non-ASCII chars, which are fragile in the age of unicode;
src/HOL/Decision_Procs/Approximation.thy
src/HOL/Library/Float.thy
src/HOL/RComplete.thy
src/HOL/ex/ApproximationEx.thy
     1.1 --- a/src/HOL/Decision_Procs/Approximation.thy	Thu Feb 26 20:55:47 2009 +0100
     1.2 +++ b/src/HOL/Decision_Procs/Approximation.thy	Thu Feb 26 20:56:59 2009 +0100
     1.3 @@ -1,7 +1,9 @@
     1.4 -(* Title:     HOL/Reflection/Approximation.thy
     1.5 - * Author:    Johannes Hölzl <hoelzl@in.tum.de> 2008 / 2009
     1.6 - *)
     1.7 +(*  Title:      HOL/Reflection/Approximation.thy
     1.8 +    Author:     Johannes Hoelzl <hoelzl@in.tum.de> 2008 / 2009
     1.9 +*)
    1.10 +
    1.11  header {* Prove unequations about real numbers by computation *}
    1.12 +
    1.13  theory Approximation
    1.14  imports Complex_Main Float Reflection Dense_Linear_Order Efficient_Nat
    1.15  begin
     2.1 --- a/src/HOL/Library/Float.thy	Thu Feb 26 20:55:47 2009 +0100
     2.2 +++ b/src/HOL/Library/Float.thy	Thu Feb 26 20:56:59 2009 +0100
     2.3 @@ -1,7 +1,7 @@
     2.4 -(* Title:    HOL/Library/Float.thy
     2.5 - * Author:   Steven Obua 2008
     2.6 - *           Johannes H\<paragraph>lzl, TU Muenchen <hoelzl@in.tum.de> 2008 / 2009
     2.7 - *)
     2.8 +(*  Title:      HOL/Library/Float.thy
     2.9 +    Author:     Steven Obua 2008
    2.10 +    Author:     Johannes Hoelzl, TU Muenchen <hoelzl@in.tum.de> 2008 / 2009
    2.11 +*)
    2.12  
    2.13  header {* Floating-Point Numbers *}
    2.14  
     3.1 --- a/src/HOL/RComplete.thy	Thu Feb 26 20:55:47 2009 +0100
     3.2 +++ b/src/HOL/RComplete.thy	Thu Feb 26 20:56:59 2009 +0100
     3.3 @@ -1,8 +1,8 @@
     3.4 -(*  Title       : HOL/RComplete.thy
     3.5 -    Author      : Jacques D. Fleuriot, University of Edinburgh
     3.6 -    Author      : Larry Paulson, University of Cambridge
     3.7 -    Author      : Jeremy Avigad, Carnegie Mellon University
     3.8 -    Author      : Florian Zuleger, Johannes Hoelzl, and Simon Funke, TU Muenchen
     3.9 +(*  Title:      HOL/RComplete.thy
    3.10 +    Author:     Jacques D. Fleuriot, University of Edinburgh
    3.11 +    Author:     Larry Paulson, University of Cambridge
    3.12 +    Author:     Jeremy Avigad, Carnegie Mellon University
    3.13 +    Author:     Florian Zuleger, Johannes Hoelzl, and Simon Funke, TU Muenchen
    3.14  *)
    3.15  
    3.16  header {* Completeness of the Reals; Floor and Ceiling Functions *}
     4.1 --- a/src/HOL/ex/ApproximationEx.thy	Thu Feb 26 20:55:47 2009 +0100
     4.2 +++ b/src/HOL/ex/ApproximationEx.thy	Thu Feb 26 20:56:59 2009 +0100
     4.3 @@ -1,6 +1,7 @@
     4.4 -(* Title:    HOL/ex/ApproximationEx.thy
     4.5 -   Author:   Johannes Hoelzl <hoelzl@in.tum.de> 2009
     4.6 +(*  Title:      HOL/ex/ApproximationEx.thy
     4.7 +    Author:     Johannes Hoelzl <hoelzl@in.tum.de> 2009
     4.8  *)
     4.9 +
    4.10  theory ApproximationEx
    4.11  imports "~~/src/HOL/Reflection/Approximation"
    4.12  begin