--- 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!