Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
standard headers;
authorwenzelm
Thu, 26 Feb 2009 20:56:59 +0100
changeset 30122 1c912a9d8200
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 file | annotate | diff | comparison | revisions
src/HOL/Library/Float.thy file | annotate | diff | comparison | revisions
src/HOL/RComplete.thy file | annotate | diff | comparison | revisions
src/HOL/ex/ApproximationEx.thy file | annotate | diff | comparison | revisions 
--- 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
--- 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 *}
 
--- 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 *}
--- 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
isabelle