forked from Isabelle_DOF/Isabelle_DOF
Update extensible record section
Update text to reflect that a property apply on the scheme type of the record
This commit is contained in:
parent
a2f3057545
commit
7033335e3f
|
@ -405,7 +405,7 @@ types. The notation for terms and types is as follows:
|
||||||
text\<open> ... where the so-called more-field \<open>\<dots>\<close> is used to 'fill-in' record-extensions.
|
text\<open> ... where the so-called more-field \<open>\<dots>\<close> is used to 'fill-in' record-extensions.
|
||||||
Schematic record types allow for simulating object-oriented features such as
|
Schematic record types allow for simulating object-oriented features such as
|
||||||
(single-)inheritance while maintaining a compositional style of verification
|
(single-)inheritance while maintaining a compositional style of verification
|
||||||
@{cite "naraschewski1998object"}: it is possible to prove a property \<^term>\<open>P (a::T)\<close>
|
@{cite "naraschewski1998object"}: it is possible to prove a property \<^term>\<open>P (z::'a T_scheme)\<close>
|
||||||
which will remain true for all extensions (which are just instances of the
|
which will remain true for all extensions (which are just instances of the
|
||||||
\<^typ>\<open>T\<close>-type).
|
\<^typ>\<open>T\<close>-type).
|
||||||
\<close>
|
\<close>
|
||||||
|
|
Reference in New Issue