summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Library/Code_Real_Approx_By_Float.thy

changeset 46530 | d5d14046686f |

parent 45496 | 5c0444d2abfe |

child 47108 | 2a1953f0d20d |

1.1 --- a/src/HOL/Library/Code_Real_Approx_By_Float.thy Sat Feb 18 23:43:21 2012 +0100 1.2 +++ b/src/HOL/Library/Code_Real_Approx_By_Float.thy Sun Feb 12 22:10:33 2012 +0100 1.3 @@ -133,11 +133,11 @@ 1.4 1.5 declare number_of_real_code [code_unfold del] 1.6 1.7 -lemma "False" 1.8 -proof- 1.9 - have "cos(pi/2) = 0" by(rule cos_pi_half) 1.10 - moreover have "cos(pi/2) \<noteq> 0" by eval 1.11 - ultimately show "False" by blast 1.12 -qed 1.13 +notepad 1.14 +begin 1.15 + have "cos (pi/2) = 0" by (rule cos_pi_half) 1.16 + moreover have "cos (pi/2) \<noteq> 0" by eval 1.17 + ultimately have "False" by blast 1.18 +end 1.19 1.20 end