equal
deleted
inserted
replaced
338 It replaces x+-y by x-y. |
338 It replaces x+-y by x-y. |
339 Addsimps [symmetric hypreal_diff_def] |
339 Addsimps [symmetric hypreal_diff_def] |
340 *) |
340 *) |
341 |
341 |
342 use "hypreal_arith.ML" |
342 use "hypreal_arith.ML" |
343 |
343 declaration {* K hypreal_arith_setup *} |
344 setup hypreal_arith_setup |
|
345 |
344 |
346 |
345 |
347 subsection {* Exponentials on the Hyperreals *} |
346 subsection {* Exponentials on the Hyperreals *} |
348 |
347 |
349 lemma hpowr_0 [simp]: "r ^ 0 = (1::hypreal)" |
348 lemma hpowr_0 [simp]: "r ^ 0 = (1::hypreal)" |