pierre.derathe
/
Isabelle_DOF
Archived
forked from Isabelle_DOF/Isabelle_DOF
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

locals

This commit is contained in:
Burkhart Wolff 2019-07-03 11:30:18 +02:00
parent a52639655f
commit 0e7f3c4cdc
1 changed files with 1 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
Isa_DOF.thy
View File

@ -1657,7 +1657,7 @@ fun check_and_mark ctxt cid_decl (str:{strict_checking: bool}) pos name =
in () end
else if DOF_core.is_declared_oid_global name thy
then (if #strict_checking str
then warning("declared but undefined document reference:"^name)(* HACK bu 29/6.19 *)
then warning("declared but undefined document reference:"^name)(* HACK bu 29/6.19 *)
else ())
else error("undefined document reference:"^name)
end