# HG changeset patch
# User wenzelm
# Date 1004043551 -7200
# Node ID 06fac365248dc08fc5bd04b6c59184bcc40b3e3e
# Parent  ff966c79cfbc0bffb805fd726a69498ab27aeaa2
accomodate some recent changes of record package;

diff -r ff966c79cfbc -r 06fac365248d doc-src/TutorialI/Types/Records.thy
--- a/doc-src/TutorialI/Types/Records.thy	Thu Oct 25 22:58:26 2001 +0200
+++ b/doc-src/TutorialI/Types/Records.thy	Thu Oct 25 22:59:11 2001 +0200
@@ -63,7 +63,7 @@
 text {* Basic simplifications. *}
 
 lemma "point.make a b = (| Xcoord = a, Ycoord = b |)"
-by simp -- "needed?? forget it"
+by (simp add: point.make_def) -- "needed?? forget it"
 
 lemma "Xcoord (| Xcoord = a, Ycoord = b |) = a"
 by simp -- "selection"
@@ -116,13 +116,13 @@
 *}
 
 constdefs
-  getX :: "('a::more) point_scheme \<Rightarrow> int"
+  getX :: "'a point_scheme \<Rightarrow> int"
    "getX r == Xcoord r"
-  setX :: "[('a::more) point_scheme, int] \<Rightarrow> 'a point_scheme"
+  setX :: "['a point_scheme, int] \<Rightarrow> 'a point_scheme"
    "setX r a == r (| Xcoord := a |)"
-  extendpt :: "'a \<Rightarrow> ('a::more) point_scheme"
+  extendpt :: "'a \<Rightarrow> 'a point_scheme"
    "extendpt ext == (| Xcoord = 15, Ycoord = 0, ... = ext |)"
-     text{*not sure what this is for!*}
+     text{*not sure what this is for!*}  (* FIXME use new point.make/extend/truncate *)
 
 
 text {*
@@ -137,11 +137,11 @@
    has its OWN more field, so a compound name is required! *}
 
 constdefs
-  incX :: "('a::more) point_scheme \<Rightarrow> 'a point_scheme"
+  incX :: "'a point_scheme \<Rightarrow> 'a point_scheme"
   "incX r == \<lparr>Xcoord = (Xcoord r) + 1, Ycoord = Ycoord r, \<dots> = point.more r\<rparr>"
 
 constdefs
-  setGreen :: "[colour, ('a::more) point_scheme] \<Rightarrow> cpoint"
+  setGreen :: "[colour, 'a point_scheme] \<Rightarrow> cpoint"
   "setGreen cl r == (| Xcoord = Xcoord r, Ycoord = Ycoord r, col = cl |)"
 
 
@@ -243,10 +243,9 @@
 So we replace the ugly manual proof by splitting.  These must be quantified: 
   the @{text "!!r"} is \emph{necessary}!  Note the occurrence of more, since
   r is polymorphic.
-*}
+*}  (* FIXME better us cases/induct *)
 lemma "!!r. r \<lparr>Xcoord := a\<rparr> = r \<lparr>Xcoord := a'\<rparr> \<Longrightarrow> a = a'"
 apply record_split --{* @{subgoals[display,indent=0,margin=65]} *}
-by simp 
-
+by simp
 
 end