Isabelle_DOF
/
Isabelle_DOF
1
0
Fork 2
Code Issues 1 Pull Requests Releases Wiki Activity

Update extensible record section 

Make it compile
This commit is contained in:
Nicolas Méric 2022-02-03 09:00:32 +01:00
parent d319ab2555
commit a2f3057545
1 changed files with 2 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
examples/scholarly_paper/2021-ITP-PMTI/paper.thy
View File

@ -405,9 +405,9 @@ 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.
Schematic record types allow for simulating object-oriented features such as
(single-)inheritance while maintaining a compositional style of verification
@{cite "naraschewski1998object"}: it is possible to prove a property \<^term>\<open>P (x::'a T\<close>
@{cite "naraschewski1998object"}: it is possible to prove a property \<^term>\<open>P (a::T)\<close>
which will remain true for all extensions (which are just instances of the
\<^typ>\<open>'a T\<close>-type).
\<^typ>\<open>T\<close>-type).
\<close>
text\<open>In \<^dof>, \<^verbatim>\<open>onto_class\<close>es and the logically equivalent \<^verbatim>\<open>doc_class\<close>es were