nicolas.meric
/
Isabelle_DOF
forked from Isabelle_DOF/Isabelle_DOF
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

debugging.

This commit is contained in:
Burkhart Wolff 2020-04-09 20:56:12 +02:00
parent d82870d1a0
commit e98e945b53
2 changed files with 3 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
src/ontologies/scholarly_paper/DOF-scholarly_paper.sty
View File

@ -220,7 +220,7 @@
\end{assertion}%
}%
{%
#1% BETTER: Since enumeration, there should be here the best possible error-msg here
ERROR CASE #1% BETTER: Since enumeration, there should be here the best possible error-msg here
}%
}%
}%

2
src/ontologies/scholarly_paper/scholarly_paper.thy
View File

@ -131,6 +131,8 @@ doc_class math_content = tc +
mcc :: "math_content_class" <= "thm"
invariant s1 :: "\<lambda> \<sigma>. \<not>referentiable \<sigma> \<longrightarrow> short_name \<sigma> = ''''"
invariant s2 :: "\<lambda> \<sigma>. status \<sigma> = semiformal"
type_synonym math_tc = math_content
text\<open>The intended use for the \<open>doc_class\<close>es \<^verbatim>\<open>math_motivation\<close> (or \<^verbatim>\<open>math_mtv\<close> for short),
\<^verbatim>\<open>math_explanation\<close> (or \<^verbatim>\<open>math_exp\<close> for short) and