src/HOL/RComplete.thy
changeset 30122 1c912a9d8200
parent 30102 799b687e4aac
child 30242 aea5d7fa7ef5
     1.1 --- a/src/HOL/RComplete.thy	Thu Feb 26 20:55:47 2009 +0100
     1.2 +++ b/src/HOL/RComplete.thy	Thu Feb 26 20:56:59 2009 +0100
     1.3 @@ -1,8 +1,8 @@
     1.4 -(*  Title       : HOL/RComplete.thy
     1.5 -    Author      : Jacques D. Fleuriot, University of Edinburgh
     1.6 -    Author      : Larry Paulson, University of Cambridge
     1.7 -    Author      : Jeremy Avigad, Carnegie Mellon University
     1.8 -    Author      : Florian Zuleger, Johannes Hoelzl, and Simon Funke, TU Muenchen
     1.9 +(*  Title:      HOL/RComplete.thy
    1.10 +    Author:     Jacques D. Fleuriot, University of Edinburgh
    1.11 +    Author:     Larry Paulson, University of Cambridge
    1.12 +    Author:     Jeremy Avigad, Carnegie Mellon University
    1.13 +    Author:     Florian Zuleger, Johannes Hoelzl, and Simon Funke, TU Muenchen
    1.14  *)
    1.15  
    1.16  header {* Completeness of the Reals; Floor and Ceiling Functions *}