changeset 21404 | eb85850d3eb7 |
parent 21243 | afffe1f72143 |
child 21454 | a1937c51ed88 |
--- a/src/HOL/Integ/IntDef.thy Fri Nov 17 02:19:55 2006 +0100 +++ b/src/HOL/Integ/IntDef.thy Fri Nov 17 02:20:03 2006 +0100 @@ -870,9 +870,11 @@ *} definition - int_aux :: "int \<Rightarrow> nat \<Rightarrow> int" + int_aux :: "int \<Rightarrow> nat \<Rightarrow> int" where "int_aux i n = (i + int n)" - nat_aux :: "nat \<Rightarrow> int \<Rightarrow> nat" + +definition + nat_aux :: "nat \<Rightarrow> int \<Rightarrow> nat" where "nat_aux n i = (n + nat i)" lemma [code]: