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

Homogenize reference style used for onto and doc classes
ci/woodpecker/push/build Pipeline was successful Details

This commit is contained in:
Nicolas Méric 2022-04-20 15:05:00 +02:00
parent 57c984d4dc
commit b448b87395
1 changed files with 1 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -398,7 +398,7 @@ types. The notation for terms and types is as follows: \<^vs>\<open>-0.2cm\<clos
\<^item> record terms \<^term>\<open>\<lparr>x = a,y = b\<rparr>\<close> and corresponding record types \<open>\<lparr>x::A, y::B\<rparr>\<close>,
\<^item> the resulting selectors are written \<^term>\<open>x(r::T)\<close>, \<^term>\<open>y(r::T)\<close>.\<close>
text\<open> \<^noindent> In fact, \<^verbatim>\<open>onto_class\<close>es and the logically equivalent \<^verbatim>\<open>doc_class\<close>es were
text\<open> \<^noindent> In fact, \<^theory_text>\<open>onto_class\<close>es and the logically equivalent \<^theory_text>\<open>doc_class\<close>es were
represented by \<^emph>\<open>extensible\<close> record types and instances thereof by HOL terms
(see @{cite"brucker.ea:isabelledof:2019"} for details.).
Invariants of an \<^verbatim>\<open>onto_class\<close> are just predicates over extensible record