src/HOL/Library/Efficient_Nat.thy
changeset 28969 4ed63cdda799
parent 28694 4e9edaef64dc
child 29258 bce03c644efb
     1.1 --- a/src/HOL/Library/Efficient_Nat.thy	Wed Dec 03 22:16:20 2008 -0800
     1.2 +++ b/src/HOL/Library/Efficient_Nat.thy	Thu Dec 04 08:47:45 2008 -0800
     1.3 @@ -349,7 +349,7 @@
     1.4  
     1.5  lemma nat_code' [code]:
     1.6    "nat (number_of l) = (if neg (number_of l \<Colon> int) then 0 else number_of l)"
     1.7 -  by auto
     1.8 +  unfolding nat_number_of_def number_of_is_id neg_def by simp
     1.9  
    1.10  lemma of_nat_int [code unfold]:
    1.11    "of_nat = int" by (simp add: int_def)