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 |