changeset 20699 | 0cc77abb185a |
parent 20640 | 05e6042394b9 |
child 20713 | 823967ef47f1 |
--- a/src/HOL/Nat.thy Mon Sep 25 17:04:14 2006 +0200 +++ b/src/HOL/Nat.thy Mon Sep 25 17:04:15 2006 +0200 @@ -1063,7 +1063,14 @@ "OperationalEquality.eq 0 (Suc m) = False" unfolding eq_def by auto code_typename - "nat" "IntDef.nat" + nat "IntDef.nat" + +code_instname + nat :: eq "IntDef.eq_nat" + nat :: ord "IntDef.ord_nat" + nat :: plus "IntDef.plus_nat" + nat :: minus "IntDef.minus_nat" + nat :: times "IntDef.times_nat" code_constname "0 \<Colon> nat" "IntDef.zero_nat"