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

more experiments
Isabelle_DOF/Isabelle_DOF/master This commit looks good Details

This commit is contained in:
Burkhart Wolff 2019-07-21 16:18:14 +02:00
parent b88031ec27
commit 869a1d6729
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/technical_report/IsaDof_Manual/04_RefMan.thy
View File

@ -559,10 +559,10 @@ In a high-level syntax, this type of constraints could be expressed, \eg, by:
\<forall> x \<in> introduction. finite(x@authored_by)
\end{isar}
@{cartouche [display=true] \<open>
\<forall> x \<in> result. x@kind = proof \<leftrightarrow> x@kind \<noteq> []
\<forall> x \<in> conclusion. \<forall> y \<in> Domain(x@establish)
\<rightarrow> \<exists> y\<in> Range(x@establish). (y,z) \<in> x@establish
\<forall> x \<in> introduction. finite(x@authored_by)
(* 1 *) \<forall> x \<in> result. x@kind = proof \<leftrightarrow> x@kind \<noteq> []
(* 2 *) \<forall> x \<in> conclusion. \<forall> y \<in> Domain(x@establish)
\<rightarrow> \<exists> y\<in> Range(x@establish). (y,z) \<in> x@establish
(* 3 *) \<forall> x \<in> introduction. finite(x@authored_by)
\<close>}
\fixme{experiment... }
where \inlineisar+result+, \inlineisar+conclusion+, and