| changeset 28229 | 4f06fae6a55e |
| parent 27651 | 16a26996c30e |
| child 28562 | 4e74209f113e |
--- a/src/HOL/NatBin.thy Tue Sep 16 09:21:24 2008 +0200 +++ b/src/HOL/NatBin.thy Tue Sep 16 09:21:26 2008 +0200 @@ -18,7 +18,7 @@ begin definition - nat_number_of_def [code inline]: "number_of v = nat (number_of v)" + nat_number_of_def [code inline, code func del]: "number_of v = nat (number_of v)" instance ..