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

Merge branch 'main' of git.logicalhacking.com:Isabelle_DOF/Isabelle_DOF
ci/woodpecker/push/build Pipeline failed Details

This commit is contained in:
Achim D. Brucker 2023-03-03 14:29:04 +00:00
parent 3b33166f55 40e7285f0a
commit 22abad9026
1 changed files with 1 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
Isabelle_DOF-Unit-Tests/Concept_OntoReferencing.thy
View File

@ -89,9 +89,7 @@ ML*[ddddd2::C]\<open>fun fac x = if x = 0 then 1 else x * (fac(x-1))\<close> (*
lemma*[ddddd3::E] asd: "True" by simp
(* BUG This does not work yet:
definition*[dddddd3::E] facu : "nat \<Rightarrow> nat" where "facu x = undefined"
*)
definition*[dddddd3::E] facu :: "nat \<Rightarrow> nat" where "facu xxxx = undefined"
(* BUG
text\<open>As shown in @{E \<open>ddddd3\<close>}\<close>