equal
deleted
inserted
replaced
70 lemma |
70 lemma |
71 defines "g \<equiv> 9.80665" and "v \<equiv> 128.61" and "d \<equiv> pi / 180" |
71 defines "g \<equiv> 9.80665" and "v \<equiv> 128.61" and "d \<equiv> pi / 180" |
72 shows "g / v * tan (35 * d) \<in> { 3 * d .. 3.1 * d }" |
72 shows "g / v * tan (35 * d) \<in> { 3 * d .. 3.1 * d }" |
73 using assms by (approximation 20) |
73 using assms by (approximation 20) |
74 |
74 |
75 lemma "x \<in> { 0 .. 1 :: real } \<longrightarrow> x ^ 2 \<le> x" |
75 lemma "x \<in> { 0 .. 1 :: real } \<longrightarrow> x\<^sup>2 \<le> x" |
76 by (approximation 30 splitting: x=1 taylor: x = 3) |
76 by (approximation 30 splitting: x=1 taylor: x = 3) |
77 |
77 |
78 value [approximate] "10" |
78 value [approximate] "10" |
79 |
79 |
80 end |
80 end |