equal
deleted
inserted
replaced
3 Author: Gertrud Bauer, TU Munich |
3 Author: Gertrud Bauer, TU Munich |
4 *) |
4 *) |
5 |
5 |
6 header {* Bounds *} |
6 header {* Bounds *} |
7 |
7 |
8 theory Bounds = Main + Real: |
8 theory Bounds imports Main Real begin |
9 |
9 |
10 locale lub = |
10 locale lub = |
11 fixes A and x |
11 fixes A and x |
12 assumes least [intro?]: "(\<And>a. a \<in> A \<Longrightarrow> a \<le> b) \<Longrightarrow> x \<le> b" |
12 assumes least [intro?]: "(\<And>a. a \<in> A \<Longrightarrow> a \<le> b) \<Longrightarrow> x \<le> b" |
13 and upper [intro?]: "a \<in> A \<Longrightarrow> a \<le> x" |
13 and upper [intro?]: "a \<in> A \<Longrightarrow> a \<le> x" |