changeset 28562 | 4e74209f113e |
parent 28229 | 4f06fae6a55e |
child 28961 | 9f33ab8e15db |
--- a/src/HOL/NatBin.thy Fri Oct 10 06:45:50 2008 +0200 +++ b/src/HOL/NatBin.thy Fri Oct 10 06:45:53 2008 +0200 @@ -18,7 +18,7 @@ begin definition - nat_number_of_def [code inline, code func del]: "number_of v = nat (number_of v)" + nat_number_of_def [code inline, code del]: "number_of v = nat (number_of v)" instance ..