summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | haftmann |

Sun, 12 Feb 2012 22:10:33 +0100 | |

changeset 46530 | d5d14046686f |

parent 46529 | a018d542e0ae |

child 46531 | eff798e48efc |

notepad is more appropriate here

--- a/src/HOL/Library/Code_Real_Approx_By_Float.thy Sat Feb 18 23:43:21 2012 +0100 +++ b/src/HOL/Library/Code_Real_Approx_By_Float.thy Sun Feb 12 22:10:33 2012 +0100 @@ -133,11 +133,11 @@ declare number_of_real_code [code_unfold del] -lemma "False" -proof- - have "cos(pi/2) = 0" by(rule cos_pi_half) - moreover have "cos(pi/2) \<noteq> 0" by eval - ultimately show "False" by blast -qed +notepad +begin + have "cos (pi/2) = 0" by (rule cos_pi_half) + moreover have "cos (pi/2) \<noteq> 0" by eval + ultimately have "False" by blast +end end