author wenzelm Sat, 01 Apr 2000 20:26:20 +0200 changeset 8659 5fdbe2dd54f9 parent 8658 3cf533397c5a child 8660 e5048a26e1d8
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)";

-
(*>*)

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

-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\$.*};```