tuned presentation;

--- a/src/HOL/Isar_examples/Summation.thy	Sat Apr 01 20:22:46 2000 +0200
+++ b/src/HOL/Isar_examples/Summation.thy	Sat Apr 01 20:26:20 2000 +0200
@@ -47,8 +47,8 @@
   "SUM i < k. b" == "sum (\\<lambda>i. b) k";
 
 
-subsection {* Summation laws *}; (*<*)
-
+subsection {* Summation laws *};
+(*<*)
 (* FIXME binary arithmetic does not yet work here *)
 
 syntax
@@ -62,7 +62,6 @@
   "6" == "Suc (Suc 4)";
 
 theorems [simp] = add_mult_distrib add_mult_distrib2 mult_ac;
-
 (*>*)
 
 text {*

--- a/src/HOL/Real/HahnBanach/Bounds.thy	Sat Apr 01 20:22:46 2000 +0200
+++ b/src/HOL/Real/HahnBanach/Bounds.thy	Sat Apr 01 20:26:20 2000 +0200
@@ -5,8 +5,8 @@
 
 header {* Bounds *};
 
-theory Bounds = Main + Real:; (*<*)
-
+theory Bounds = Main + Real:;
+(*<*)
 subsection {* The sets of lower and upper bounds *};
 
 constdefs
@@ -66,7 +66,6 @@
 
 
 subsection {* Infimum and Supremum *};
-
 (*>*)
 text {*
  A supremum\footnote{The definition of the supremum is based on one in
@@ -83,8 +82,8 @@
   "is_Sup A B x == isLub A B x"
 
   Sup :: "('a::order) set => 'a set => 'a"
-  "Sup A B == Eps (is_Sup A B)"; (*<*)
-
+  "Sup A B == Eps (is_Sup A B)";
+(*<*)
 constdefs
   is_Inf :: "('a::order) set => 'a set => 'a => bool"
   "is_Inf A B x == x:A & is_Greatest (LowerBounds A B) x"
@@ -107,7 +106,6 @@
   "SUP x. P" == "SUP x:UNIV. P"
   "INF x:A. P" == "Inf A (Collect (\<lambda>x. P))"
   "INF x. P" == "INF x:UNIV. P";
-
 (*>*)
 text{* The supremum of $B$ is less than any upper bound
 of $B$.*};