src/HOL/Library/Type_Length.thy
changeset 70348 bde161c740ca
parent 69597 ff784d5a5bfb
     1.1 --- a/src/HOL/Library/Type_Length.thy	Fri Jun 14 08:34:28 2019 +0000
     1.2 +++ b/src/HOL/Library/Type_Length.thy	Fri Jun 14 08:34:28 2019 +0000
     1.3 @@ -33,6 +33,13 @@
     1.4  
     1.5  class len = len0 +
     1.6    assumes len_gt_0 [iff]: "0 < LENGTH('a)"
     1.7 +begin
     1.8 +
     1.9 +lemma len_not_eq_0 [simp]:
    1.10 +  "LENGTH('a) \<noteq> 0"
    1.11 +  by simp
    1.12 +
    1.13 +end
    1.14  
    1.15  instantiation num0 and num1 :: len0
    1.16  begin