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

Fix typo
ci/woodpecker/push/build Pipeline was successful Details

This commit is contained in:
Nicolas Méric 2022-04-07 14:29:24 +02:00
parent 65e6240fa8
commit 7201101a6c
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

@ -540,7 +540,7 @@ text\<open>
We provide the equivalent commands, respectively \<^theory_text>\<open>term*\<close> and \<^theory_text>\<open>value*\<close>, which
additionally support a validation and elaboration phase.
We also provide an \<^theory_text>\<open>assert*\<close>-command which checks
that the evaluation of a term returns \<^const>\<open>True\<close> and fails in other cases.
that the evaluation of a term returns \<^const>\<open>True\<close> and fails otherwise.
Note that term antiquotations are admitted in all \<^dof> commands, not just
\<^theory_text>\<open>term*\<close>, \<^theory_text>\<open>value*\<close> and \<^theory_text>\<open>assert*\<close>.
\<close>