equal
deleted
inserted
replaced
68 apply (subst hypreal_of_real_le_iff [symmetric]) |
68 apply (subst hypreal_of_real_le_iff [symmetric]) |
69 apply (simp (no_asm)) |
69 apply (simp (no_asm)) |
70 done |
70 done |
71 |
71 |
72 subsection{*Absolute Value Function for the Hyperreals*} |
72 subsection{*Absolute Value Function for the Hyperreals*} |
73 |
|
74 declare abs_mult [simp] |
|
75 |
73 |
76 lemma hrabs_add_less: |
74 lemma hrabs_add_less: |
77 "[| abs x < r; abs y < s |] ==> abs(x+y) < r + (s::hypreal)" |
75 "[| abs x < r; abs y < s |] ==> abs(x+y) < r + (s::hypreal)" |
78 by (simp add: abs_if split: split_if_asm) |
76 by (simp add: abs_if split: split_if_asm) |
79 |
77 |