author wenzelm Sun, 26 Mar 2000 20:17:52 +0200 changeset 8585 8a3ae21e4a5b parent 8584 016314c2fa0a child 8586 e451c4865548
tuned presentation;
--- a/src/HOL/Real/HahnBanach/Bounds.thy	Sun Mar 26 20:16:34 2000 +0200
+++ b/src/HOL/Real/HahnBanach/Bounds.thy	Sun Mar 26 20:17:52 2000 +0200
@@ -5,9 +5,7 @@

header {* Bounds *};

-theory Bounds = Main + Real:;
-
-text_raw {* \begin{comment} *};
+theory Bounds = Main + Real:; (*<*)

subsection {* The sets of lower and upper bounds *};

@@ -69,8 +67,7 @@

subsection {* Infimum and Supremum *};

-text_raw {* \end{comment} *};
-
+(*>*)
text {*
A supremum\footnote{The definition of the supremum is based on one in
\url{http://isabelle.in.tum.de/library/HOL/HOL-Real/Lubs.html}}  of
@@ -86,9 +83,7 @@
"is_Sup A B x == isLub A B x"

Sup :: "('a::order) set => 'a set => 'a"
-  "Sup A B == Eps (is_Sup A B)";
-;
-text_raw {* \begin{comment} *};
+  "Sup A B == Eps (is_Sup A B)"; (*<*)

constdefs
is_Inf :: "('a::order) set => 'a set => 'a => bool"
@@ -113,9 +108,7 @@
"INF x:A. P" == "Inf A (Collect (\<lambda>x. P))"
"INF x. P" == "INF x:UNIV. P";

-text_raw {* \end{comment} *};
-;
-
+(*>*)
text{* The supremum of $B$ is less than any upper bound
of $B$.*};

--- a/src/HOL/Real/HahnBanach/document/root.tex	Sun Mar 26 20:16:34 2000 +0200
+++ b/src/HOL/Real/HahnBanach/document/root.tex	Sun Mar 26 20:17:52 2000 +0200
@@ -1,7 +1,6 @@

\documentclass[11pt,a4paper,twoside]{article}

-\usepackage{comment}
\usepackage{latexsym,theorem}
\usepackage{isabelle,isabellesym,bbb}
\usepackage{pdfsetup} %last one!