src/HOL/ex/Records.thy

--- a/src/HOL/ex/Records.thy	Fri Nov 17 02:19:55 2006 +0100
+++ b/src/HOL/ex/Records.thy	Fri Nov 17 02:20:03 2006 +0100
@@ -51,9 +51,11 @@
 subsubsection {* Record selection and record update *}
 
 definition
-  getX :: "'a point_scheme => nat"
+  getX :: "'a point_scheme => nat" where
   "getX r = xpos r"
-  setX :: "'a point_scheme => nat => 'a point_scheme"
+
+definition
+  setX :: "'a point_scheme => nat => 'a point_scheme" where
   "setX r n = r (| xpos := n |)"
 
 
@@ -145,14 +147,14 @@
 *}
 
 definition
-  foo5 :: nat
+  foo5 :: nat where
   "foo5 = getX (| xpos = 1, ypos = 0 |)"
 
 
 text {* \medskip Manipulating the ``@{text "..."}'' (more) part. *}
 
 definition
-  incX :: "'a point_scheme => 'a point_scheme"
+  incX :: "'a point_scheme => 'a point_scheme" where
   "incX r = (| xpos = xpos r + 1, ypos = ypos r, ... = point.more r |)"
 
 lemma "incX r = setX r (Suc (getX r))"
@@ -162,7 +164,7 @@
 text {* An alternative definition. *}
 
 definition
-  incX' :: "'a point_scheme => 'a point_scheme"
+  incX' :: "'a point_scheme => 'a point_scheme" where
   "incX' r = r (| xpos := xpos r + 1 |)"
 
 
@@ -194,7 +196,7 @@
 *}
 
 definition
-  foo10 :: nat
+  foo10 :: nat where
   "foo10 = getX (| xpos = 2, ypos = 0, colour = Blue |)"
 
 
@@ -206,7 +208,7 @@
 *}
 
 definition
-  foo11 :: cpoint
+  foo11 :: cpoint where
   "foo11 = setX (| xpos = 2, ypos = 0, colour = Blue |) 0"