# HG changeset patch
# User wenzelm
# Date 954094672 -7200
# Node ID 8a3ae21e4a5ba8da2c7db2814152f309b9592b15
# Parent  016314c2fa0a5ae8060728150b05e6705055987f
tuned presentation;

diff -r 016314c2fa0a -r 8a3ae21e4a5b src/HOL/Real/HahnBanach/Bounds.thy
--- 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$.*};
 
diff -r 016314c2fa0a -r 8a3ae21e4a5b src/HOL/Real/HahnBanach/document/root.tex
--- 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!