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

Update invariants section

This commit is contained in:
Nicolas Méric 2022-02-04 17:41:43 +01:00
parent 33d991a1c7
commit 94baf69f25
1 changed files with 3 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -709,7 +709,7 @@ figure*[
"invariant-checking-figure"::figure
, relative_width="99"
, src="''figures/invariant-checking-violated-example''"
]\<open>The invariant \<^theory_text>\<open>force_level\<close> of the class \<^theory_text>\<open>introduction\<close> is violated by
]\<open>The \<^theory_text>\<open>invariant force_level\<close> of the class \<^theory_text>\<open>myintroduction\<close> is violated by
the instance \<^theory_text>\<open>introduction1\<close>.\<close>
(*<*)
@ -729,8 +729,8 @@ figure*[
"inherited-invariant-checking-figure"::figure
, relative_width="99"
, src="''figures/inherited-invariant-checking-violated-example''"
]\<open>The invariant \<^theory_text>\<open>force_level\<close> of the class claim is inherited
from the class \<^theory_text>\<open>introduction\<close> and is violated by the instance \<^theory_text>\<open>claimNotion\<close>.
]\<open>The \<^theory_text>\<open>invariant force_level\<close> of the class \<^theory_text>\<open>myclaim\<close> is inherited
from the class \<^theory_text>\<open>myintroduction\<close> and is violated by the instance \<^theory_text>\<open>claimNotion\<close>.
\<close>
(*<*)