equal
deleted
inserted
replaced
1 |
1 |
2 theory HyperArith = HyperArith0 |
2 theory HyperArith = HyperArith0 |
3 files "hypreal_arith.ML": |
3 files "hypreal_arith.ML": |
4 |
4 |
5 setup hypreal_arith_setup |
5 setup hypreal_arith_setup |
|
6 |
|
7 text{*Used once in NSA*} |
|
8 lemma hypreal_add_minus_eq_minus: "x + y = (0::hypreal) ==> x = -y" |
|
9 apply arith |
|
10 done |
|
11 |
|
12 ML |
|
13 {* |
|
14 val hypreal_add_minus_eq_minus = thm "hypreal_add_minus_eq_minus"; |
|
15 *} |
6 |
16 |
7 subsubsection{*Division By @{term 1} and @{term "-1"}*} |
17 subsubsection{*Division By @{term 1} and @{term "-1"}*} |
8 |
18 |
9 lemma hypreal_divide_minus1 [simp]: "x/-1 = -(x::hypreal)" |
19 lemma hypreal_divide_minus1 [simp]: "x/-1 = -(x::hypreal)" |
10 by simp |
20 by simp |