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

Homogenize refrence style for onto class
ci/woodpecker/push/build Pipeline was successful Details

This commit is contained in:
Nicolas Méric 2022-04-20 15:06:34 +02:00
parent b448b87395
commit f30ff6a967
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

@ -401,7 +401,7 @@ types. The notation for terms and types is as follows: \<^vs>\<open>-0.2cm\<clos
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
Invariants of an \<^theory_text>\<open>onto_class\<close> are just predicates over extensible record
types and were applied to subclasses. \<close>
subsection\<open>Term-Evaluations in Isabelle\<close>