doc-src/TutorialI/Advanced/Partial.thy

--- a/doc-src/TutorialI/Advanced/Partial.thy	Wed Feb 24 11:55:52 2010 +0100
+++ b/doc-src/TutorialI/Advanced/Partial.thy	Mon Mar 01 13:40:23 2010 +0100
@@ -34,7 +34,7 @@
 preconditions:
 *}
 
-constdefs subtract :: "nat \<Rightarrow> nat \<Rightarrow> nat"
+definition subtract :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
 "n \<le> m \<Longrightarrow> subtract m n \<equiv> m - n"
 
 text{*
@@ -85,7 +85,7 @@
 Phrased differently, the relation
 *}
 
-constdefs step1 :: "('a \<Rightarrow> 'a) \<Rightarrow> ('a \<times> 'a)set"
+definition step1 :: "('a \<Rightarrow> 'a) \<Rightarrow> ('a \<times> 'a)set" where
   "step1 f \<equiv> {(y,x). y = f x \<and> y \<noteq> x}"
 
 text{*\noindent
@@ -160,7 +160,7 @@
 consider the following definition of function @{const find}:
 *}
 
-constdefs find2 :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a"
+definition find2 :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" where
   "find2 f x \<equiv>
    fst(while (\<lambda>(x,x'). x' \<noteq> x) (\<lambda>(x,x'). (x',f x')) (x,f x))"