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

author | haftmann |

Fri, 19 Oct 2007 07:48:23 +0200 | |

changeset 25089 | 04b8456f7754 |

parent 25088 | 9a13ab12b174 |

child 25090 | 4a50b958391a |

dropped doubled proof

--- a/src/HOL/Numeral.thy Thu Oct 18 17:44:30 2007 +0200 +++ b/src/HOL/Numeral.thy Fri Oct 19 07:48:23 2007 +0200 @@ -325,13 +325,7 @@ subsection {* Comparisons, for Ordered Rings *} -lemma double_eq_0_iff: - "(a + a = 0) = (a = (0::'a::ordered_idom))" -proof - - have "a + a = (1 + 1) * a" unfolding left_distrib by simp - with zero_less_two [where 'a = 'a] - show ?thesis by force -qed +lemmas double_eq_0_iff = double_zero lemma le_imp_0_less: assumes le: "0 \<le> z"