equal
deleted
inserted
replaced
8 theory Aux = Real + Zorn: |
8 theory Aux = Real + Zorn: |
9 |
9 |
10 text {* Some existing theorems are declared as extra introduction |
10 text {* Some existing theorems are declared as extra introduction |
11 or elimination rules, respectively. *} |
11 or elimination rules, respectively. *} |
12 |
12 |
13 lemmas [intro??] = isLub_isUb |
13 lemmas [intro?] = isLub_isUb |
14 lemmas [intro??] = chainD |
14 lemmas [intro?] = chainD |
15 lemmas chainE2 = chainD2 [elimify] |
15 lemmas chainE2 = chainD2 [elimify] |
16 |
16 |
17 text_raw {* \medskip *} |
17 text_raw {* \medskip *} |
18 text{* Lemmas about sets. *} |
18 text{* Lemmas about sets. *} |
19 |
19 |