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

Fix typo

This commit is contained in:
Nicolas Méric 2022-03-15 08:31:16 +01:00
parent 913bf49b3f
commit f96db62396
1 changed files with 4 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -770,14 +770,14 @@ value*\<open>filter (\<lambda>\<sigma>. myresult.evidence \<sigma> = argument) @
text\<open>
Any class definition generates term antiquotations checking a class instance or
to the set of instances in a particular logical context; these references were
the set of instances in a particular logical context; these references were
elaborated to objects they refer to.
This paves the way for a new mechanism to query the ``current'' instances presented as a
list of \<^hol> \<^type>\<open>list\<close>.
Arbitrarily Complex queries can therefore be defined inside the logical language.
Arbitrarily complex queries can therefore be defined inside the logical language.
Thus, to get the list of the properties of the instances of the class \<^typ>\<open>myresult\<close>,
it suffices to get the list of the authors of the instances of the \<^typ>\<open>myintroduction\<close> class,
and to treat this meta-data as usual:
or to get the list of the authors of the instances of the \<^typ>\<open>myintroduction\<close> class,
it suffices to treat this meta-data as usual:
@{theory_text [display,indent=5, margin=70] \<open>
value*\<open>map (myresult.property) @{myresult-instances}\<close>
value*\<open>map (mytext_section.authored_by) @{myintroduction-instances}\<close>