| changeset 13596 | ee5f79b210c1 |
| parent 13585 | db4005b40cc6 |
| child 14131 | a4fc8b1af5e7 |
--- a/src/HOL/Nat.thy Fri Sep 27 16:44:50 2002 +0200 +++ b/src/HOL/Nat.thy Mon Sep 30 15:44:21 2002 +0200 @@ -448,7 +448,6 @@ by (blast dest!: le_imp_less_or_eq intro: less_or_eq_imp_le less_trans) lemma le_anti_sym: "[| m <= n; n <= m |] ==> m = (n::nat)" - -- {* @{text order_less_irrefl} could make this proof fail *} by (blast dest!: le_imp_less_or_eq elim!: less_irrefl elim: less_asym) lemma Suc_le_mono [iff]: "(Suc n <= Suc m) = (n <= m)"