changeset 70348 | bde161c740ca |
parent 69597 | ff784d5a5bfb |
child 70901 | 94a0c47b8553 |
--- a/src/HOL/Library/Type_Length.thy Fri Jun 14 08:34:28 2019 +0000 +++ b/src/HOL/Library/Type_Length.thy Fri Jun 14 08:34:28 2019 +0000 @@ -33,6 +33,13 @@ class len = len0 + assumes len_gt_0 [iff]: "0 < LENGTH('a)" +begin + +lemma len_not_eq_0 [simp]: + "LENGTH('a) \<noteq> 0" + by simp + +end instantiation num0 and num1 :: len0 begin