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-02-08 11:04:24 +01:00
parent 4edcb1acd1
commit e511049ba8
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

@ -1208,7 +1208,7 @@ text\<open> We plan to complement \<^dof> with incremental LaTeX generation and
that will further increase the usability of our framework for the ontology-conform editing
of formal content, be it in the engineering or the mathematics domain.
Another line of future application is to increase the ``depth'' of build-in term antiquotations such
Another line of future application is to increase the ``depth'' of built-in term antiquotations such
as \<^theory_text>\<open>@{typ \<open>'\<tau>\<close>}\<close>, \<^term>\<open>@{term \<open>a + b\<close>}\<close> and \<^term>\<open>@{thm \<open>HOL.refl\<close>}\<close>, which are currently implemented just as
validations in the current logical context. In the future, they could optionally be expanded to
the types, terms and theorems (with proof objects attached) in a meta-model of the Isabelle Kernel