Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Library/Efficient_Nat.thy
changeset 28969 4ed63cdda799
parent 28694 4e9edaef64dc
child 29258 bce03c644efb 
--- a/src/HOL/Library/Efficient_Nat.thy	Wed Dec 03 22:16:20 2008 -0800
+++ b/src/HOL/Library/Efficient_Nat.thy	Thu Dec 04 08:47:45 2008 -0800
@@ -349,7 +349,7 @@
 
 lemma nat_code' [code]:
   "nat (number_of l) = (if neg (number_of l \<Colon> int) then 0 else number_of l)"
-  by auto
+  unfolding nat_number_of_def number_of_is_id neg_def by simp
 
 lemma of_nat_int [code unfold]:
   "of_nat = int" by (simp add: int_def)
isabelle