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

...

This commit is contained in:
Burkhart Wolff 2022-04-06 09:29:10 +02:00
parent b3fd073b38
commit 74ba9aa892
3 changed files with 4 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
examples/scholarly_paper/2020-iFM-CSP/paper.thy
View File

@ -3,7 +3,6 @@ theory "paper"
imports "Isabelle_DOF.scholarly_paper"
begin
open_monitor*[this::article]
declare[[ strict_monitor_checking = false]]

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

@ -17,6 +17,7 @@ define_shortcut* hol \<rightleftharpoons> \<open>HOL\<close>
html \<rightleftharpoons> \<open>HTML\<close>
csp \<rightleftharpoons> \<open>CSP\<close> \<comment>\<open>obsolete\<close>
holcsp \<rightleftharpoons> \<open>HOL-CSP\<close> \<comment>\<open>obsolete\<close>
ML\<open>

4
src/tests/Evaluation.thy
View File

@ -200,7 +200,9 @@ text\<open>Assertions must be true, hence the error:\<close>
assert*\<open>{@{author \<open>curry\<close>}} = {@{author \<open>church\<close>}}\<close>*)
term*\<open>property @{result \<open>resultProof\<close>} = property @{result \<open>resultProof2\<close>}\<close>
assert*\<open>\<not> property @{result \<open>resultProof\<close>} = property @{result \<open>resultProof2\<close>}\<close>
assert*[ass::A]\<open>\<not> property @{result \<open>resultProof\<close>} = property @{result \<open>resultProof2\<close>}\<close>
text\<open>@{A [display] "ass"}}\<close>
assert*\<open>evidence @{result \<open>resultProof\<close>} = evidence @{result \<open>resultProof2\<close>}\<close>