changeset 28562 | 4e74209f113e |
parent 28514 | da83a614c454 |
child 28823 | dcbef866c9e2 |
--- a/src/HOL/Nat.thy Fri Oct 10 06:45:50 2008 +0200 +++ b/src/HOL/Nat.thy Fri Oct 10 06:45:53 2008 +0200 @@ -55,7 +55,7 @@ instantiation nat :: zero begin -definition Zero_nat_def [code func del]: +definition Zero_nat_def [code del]: "0 = Abs_Nat Zero_Rep" instance .. @@ -1281,7 +1281,7 @@ definition Nats :: "'a set" where - [code func del]: "Nats = range of_nat" + [code del]: "Nats = range of_nat" notation (xsymbols) Nats ("\<nat>")