equal
deleted
inserted
replaced
62 |
62 |
63 lemma "(1234567::real) \<le> 1234567" |
63 lemma "(1234567::real) \<le> 1234567" |
64 by simp |
64 by simp |
65 |
65 |
66 |
66 |
|
67 text {* \medskip Powers *} |
|
68 |
|
69 lemma "2 ^ 15 = (32768::real)" |
|
70 by simp |
|
71 |
|
72 lemma "-3 ^ 7 = (-2187::real)" |
|
73 by simp |
|
74 |
|
75 lemma "13 ^ 7 = (62748517::real)" |
|
76 by simp |
|
77 |
|
78 lemma "3 ^ 15 = (14348907::real)" |
|
79 by simp |
|
80 |
|
81 lemma "-5 ^ 11 = (-48828125::real)" |
|
82 by simp |
|
83 |
|
84 |
67 text {* \medskip Tests *} |
85 text {* \medskip Tests *} |
68 |
86 |
69 lemma "(x + y = x) = (y = (0::real))" |
87 lemma "(x + y = x) = (y = (0::real))" |
70 by arith |
88 by arith |
71 |
89 |