equal
deleted
inserted
replaced
138 have "cos(pi/2) = 0" by(rule cos_pi_half) |
138 have "cos(pi/2) = 0" by(rule cos_pi_half) |
139 moreover have "cos(pi/2) \<noteq> 0" by eval |
139 moreover have "cos(pi/2) \<noteq> 0" by eval |
140 ultimately show "False" by blast |
140 ultimately show "False" by blast |
141 qed |
141 qed |
142 |
142 |
143 definition "test = exp (sin 3) / 5 * cos 6 + arctan (arccos (arcsin 8))" |
143 lemma False |
144 |
144 sorry -- "Use quick_and_dirty to load this theory." |
145 export_code test |
|
146 in OCaml file - |
|
147 |
145 |
148 end |
146 end |