equal
deleted
inserted
replaced
12 begin |
12 begin |
13 |
13 |
14 text {* |
14 text {* |
15 This theory contains a formalization of the real numbers as |
15 This theory contains a formalization of the real numbers as |
16 equivalence classes of Cauchy sequences of rationals. See |
16 equivalence classes of Cauchy sequences of rationals. See |
17 \url{HOL/ex/Dedekind_Real.thy} for an alternative construction |
17 @{file "~~/src/HOL/ex/Dedekind_Real.thy"} for an alternative |
18 using Dedekind cuts. |
18 construction using Dedekind cuts. |
19 *} |
19 *} |
20 |
20 |
21 subsection {* Preliminary lemmas *} |
21 subsection {* Preliminary lemmas *} |
22 |
22 |
23 lemma add_diff_add: |
23 lemma add_diff_add: |