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

Reactivating failing assertions

This commit is contained in:
Burkhart Wolff 2023-03-24 17:21:36 +01:00
parent 5628eaa2dc
commit 81a50c6a9e
1 changed files with 4 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
Isabelle_DOF-Unit-Tests/AssnsLemmaThmEtc.thy
View File

@ -40,9 +40,12 @@ in the assertion.
\<close>
ML\<open>
@{term "[@{term '' True @<longrightarrow> True ''}]"}; (* with isa-check *)
@{term "[@{term \<open>True \<longrightarrow> True \<close>}]"}; (* with isa-check *)
\<close>
Definition*[ertert]\<open>dfgdfg\<close>
Theorem*[dgdfgddfg]\<open>dfgdfg\<close>
lemma "All (\<lambda>x. X \<and> Y \<longrightarrow> True)" oops