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

improved layout
Isabelle_DOF/Isabelle_DOF/master This commit looks good Details

This commit is contained in:
Burkhart Wolff 2019-08-15 11:44:29 +02:00
parent 6414e1e568
commit 1da0433451
1 changed files with 3 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy
View File

@ -472,9 +472,10 @@ text*[claim::assertions]\<open>For non-empty lists, our definition yields indeed
assert*[claim::assertions] "last[4::int] = 4"
assert*[claim::assertions] "last[1,2,3,4::int] = 4"
(*>*)
text\<open>We want to check the consequences of this definition and can add the following sdtatements:
text\<open>We want to check the consequences of this definition and can add the following statements:
\begin{isar}
text*[claim::assertions]\<open>For non-empty lists, our definition yields indeed the last element of a list.\<close>
text*[claim::assertions]\<Open>For non-empty lists, our definition yields indeed
the last element of a list.\<Close>
assert*[claim::assertions] "last[4::int] = 4"
assert*[claim::assertions] "last[1,2,3,4::int] = 4"
\end{isar}