changeset 27682 | 25aceefd4786 |
parent 27368 | 9f90ac19e32b |
child 28562 | 4e74209f113e |
--- a/src/HOL/Library/Char_ord.thy Fri Jul 25 12:03:32 2008 +0200 +++ b/src/HOL/Library/Char_ord.thy Fri Jul 25 12:03:34 2008 +0200 @@ -35,7 +35,7 @@ by (auto simp add: nat_of_nibble_eq) next fix n m :: nibble - show "n < m \<longleftrightarrow> n \<le> m \<and> n \<noteq> m" + show "n < m \<longleftrightarrow> n \<le> m \<and> \<not> m \<le> n" unfolding nibble_less_eq_def nibble_less_def less_le by (auto simp add: nat_of_nibble_eq) next