src/HOL/ex/Records.thy
changeset 11701 3d51fbf81c17
parent 10357 0d0cac129618
child 11704 3c50a2cd6f00
equal deleted inserted replaced
11700:a0e6bda62b7b 11701:3d51fbf81c17
   180  Functions on @{text point} schemes work for @{text cpoints} as well.
   180  Functions on @{text point} schemes work for @{text cpoints} as well.
   181 *}
   181 *}
   182 
   182 
   183 constdefs
   183 constdefs
   184   foo10 :: nat
   184   foo10 :: nat
   185   "foo10 == getX (| x = 2, y = 0, colour = Blue |)"
   185   "foo10 == getX (| x = # 2, y = 0, colour = Blue |)"
   186 
   186 
   187 
   187 
   188 subsubsection {* Non-coercive structural subtyping *}
   188 subsubsection {* Non-coercive structural subtyping *}
   189 
   189 
   190 text {*
   190 text {*
   192  Great!
   192  Great!
   193 *}
   193 *}
   194 
   194 
   195 constdefs
   195 constdefs
   196   foo11 :: cpoint
   196   foo11 :: cpoint
   197   "foo11 == setX (| x = 2, y = 0, colour = Blue |) 0"
   197   "foo11 == setX (| x = # 2, y = 0, colour = Blue |) 0"
   198 
   198 
   199 
   199 
   200 subsection {* Other features *}
   200 subsection {* Other features *}
   201 
   201 
   202 text {* Field names contribute to record identity. *}
   202 text {* Field names contribute to record identity. *}
   205   x' :: nat
   205   x' :: nat
   206   y' :: nat
   206   y' :: nat
   207 
   207 
   208 text {*
   208 text {*
   209  \noindent May not apply @{term getX} to 
   209  \noindent May not apply @{term getX} to 
   210  @{term [source] "(| x' = 2, y' = 0 |)"}.
   210  @{term [source] "(| x' = # 2, y' = 0 |)"}.
   211 *}
   211 *}
   212 
   212 
   213 text {* \medskip Polymorphic records. *}
   213 text {* \medskip Polymorphic records. *}
   214 
   214 
   215 record 'a point'' = point +
   215 record 'a point'' = point +