--- a/src/HOL/NatBin.thy Fri Jan 25 14:53:58 2008 +0100
+++ b/src/HOL/NatBin.thy Fri Jan 25 14:54:41 2008 +0100
@@ -18,12 +18,16 @@
begin
definition
- nat_number_of_def [code inline]: "number_of v = nat (number_of (v\<Colon>int))"
+ nat_number_of_def [code inline]: "number_of v = nat (number_of v)"
instance ..
end
+lemma [code post]:
+ "nat (number_of v) = number_of v"
+ unfolding nat_number_of_def ..
+
abbreviation (xsymbols)
square :: "'a::power => 'a" ("(_\<twosuperior>)" [1000] 999) where
"x\<twosuperior> == x^2"