equal
deleted
inserted
replaced
39 |
39 |
40 (*standard real numbers as a subset of the hyperreals*) |
40 (*standard real numbers as a subset of the hyperreals*) |
41 SReal_def: "Reals == {x. \<exists>r. x = hypreal_of_real r}" |
41 SReal_def: "Reals == {x. \<exists>r. x = hypreal_of_real r}" |
42 |
42 |
43 syntax (xsymbols) |
43 syntax (xsymbols) |
|
44 approx :: "[hypreal, hypreal] => bool" (infixl "\<approx>" 50) |
|
45 |
|
46 syntax (HTML output) |
44 approx :: "[hypreal, hypreal] => bool" (infixl "\<approx>" 50) |
47 approx :: "[hypreal, hypreal] => bool" (infixl "\<approx>" 50) |
45 |
48 |
46 |
49 |
47 |
50 |
48 subsection{*Closure Laws for Standard Reals*} |
51 subsection{*Closure Laws for Standard Reals*} |