equal
deleted
inserted
replaced
102 It replaces x+-y by x-y. |
102 It replaces x+-y by x-y. |
103 Addsimps [symmetric hypreal_diff_def] |
103 Addsimps [symmetric hypreal_diff_def] |
104 *) |
104 *) |
105 |
105 |
106 |
106 |
107 subsection{*Numerals and Arithmetic*} |
|
108 |
|
109 lemma star_of_zero: "star_of 0 = 0" |
|
110 by simp |
|
111 |
|
112 lemma star_of_one: "star_of 1 = 1" |
|
113 by simp |
|
114 |
|
115 lemma star_of_add: "star_of (x + y) = star_of x + star_of y" |
|
116 by simp |
|
117 |
|
118 lemma star_of_minus: "star_of (- x) = - star_of x" |
|
119 by simp |
|
120 |
|
121 lemma star_of_diff: "star_of (x - y) = star_of x - star_of y" |
|
122 by simp |
|
123 |
|
124 lemma star_of_mult: "star_of (x * y) = star_of x * star_of y" |
|
125 by simp |
|
126 |
|
127 lemma star_of_number_of: "star_of (number_of v) = number_of v" |
|
128 by simp |
|
129 |
|
130 use "hypreal_arith.ML" |
107 use "hypreal_arith.ML" |
131 |
108 |
132 setup hypreal_arith_setup |
109 setup hypreal_arith_setup |
133 |
110 |
134 end |
111 end |