| changeset 32069 | 6d28bbd33e2c |
| parent 31998 | 2c7a24f74db9 |
| child 33296 | a3924d1069e5 |
--- a/src/HOL/Nat_Numeral.thy Tue Jul 14 16:27:31 2009 +0200 +++ b/src/HOL/Nat_Numeral.thy Tue Jul 14 16:27:32 2009 +0200 @@ -20,7 +20,7 @@ begin definition - nat_number_of_def [code_inline, code del]: "number_of v = nat (number_of v)" + nat_number_of_def [code_unfold, code del]: "number_of v = nat (number_of v)" instance ..