diff -r dd58f13a8eb4 -r eb85850d3eb7 src/HOL/ex/Abstract_NAT.thy
--- a/src/HOL/ex/Abstract_NAT.thy	Fri Nov 17 02:19:55 2006 +0100
+++ b/src/HOL/ex/Abstract_NAT.thy	Fri Nov 17 02:20:03 2006 +0100
@@ -66,7 +66,7 @@
 text {* \medskip The recursion operator -- polymorphic! *}
 
 definition
-  rec :: "'a \<Rightarrow> ('n \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'n \<Rightarrow> 'a"
+  rec :: "'a \<Rightarrow> ('n \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'n \<Rightarrow> 'a" where
   "rec e r x = (THE y. Rec e r x y)"
 
 lemma rec_eval:
@@ -92,7 +92,7 @@
 text {* \medskip Example: addition (monomorphic) *}
 
 definition
-  add :: "'n \<Rightarrow> 'n \<Rightarrow> 'n"
+  add :: "'n \<Rightarrow> 'n \<Rightarrow> 'n" where
   "add m n = rec n (\<lambda>_ k. succ k) m"
 
 lemma add_zero [simp]: "add zero n = n"
@@ -116,7 +116,7 @@
 text {* \medskip Example: replication (polymorphic) *}
 
 definition
-  repl :: "'n \<Rightarrow> 'a \<Rightarrow> 'a list"
+  repl :: "'n \<Rightarrow> 'a \<Rightarrow> 'a list" where
   "repl n x = rec [] (\<lambda>_ xs. x # xs) n"
 
 lemma repl_zero [simp]: "repl zero x = []"