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

support for math_example into the Urschleim.

This commit is contained in:
Burkhart Wolff 2020-04-09 18:12:14 +02:00
parent f1b376d4b6
commit d82870d1a0
2 changed files with 30 additions and 30 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -231,37 +231,36 @@
\end{isamarkuptext}%
}
%\newisadof{text.scholarly_paper.math_content}%
%[label=,type=%
% , scholarly_paper.math_content.short_name ={} % or \relax
% , scholarly_paper.math_content.mcc =%
% , Isa_COL.text_element.level =%
% , Isa_COL.text_element.referentiable =%
% , Isa_COL.text_element.variants =%
% , scholarly_paper.text_section.main_author =%
% , scholarly_paper.text_section.fixme_list =%
% , Isa_COL.text_element.level =%
% , scholarly_paper.technical.definition_list =%
% , scholarly_paper.technical.status =%
% ]
% [1]
% {%
% \begin{isamarkuptext}%
% \ifthenelse{\equal{\commandkey{scholarly_paper.math_content.mcc}}{def}}{
% \ifthenelse{\equal{\commandkey{scholarly_paper.math_content.short_name}} {} }
% {\begin{definition} \label{\commandkey{label}} #1 \end{definition} }
% {\begin{definition} [\commandkey{scholarly_paper.math_content.short_name}]
% \label{\commandkey{label}} #1
% \end{definition}}
% }{%
% #1%
% }%
% \end{isamarkuptext}%
% }
% end: scholarly_paper.abstract
% end: scholarly_paper.math_content
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newisadof{text.scholarly_paper.math_example}%
[label=,type=%
, scholarly_paper.math_example.short_name =%
, Isa_COL.text_element.level =%
, Isa_COL.text_element.referentiable =%
, Isa_COL.text_element.variants =%
, scholarly_paper.text_section.main_author =%
, scholarly_paper.text_section.fixme_list =%
, scholarly_paper.technical.definition_list =%
, scholarly_paper.technical.status =%
]
[1]
{%
\begin{isamarkuptext}%
\ifthenelse{\equal{\commandkey{scholarly_paper.technical.status}}{semiformal}}{
\ifthenelse{\equal{\commandkey{scholarly_paper.math_example.short_name}} {} }
{\begin{example} \label{\commandkey{label}} #1 \end{example} }
{\begin{example} [\commandkey{scholarly_paper.math_example.short_name}]
\label{\commandkey{label}} #1
\end{example}}
}{%
#1%
}%
\end{isamarkuptext}%
}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newisadof{text.scholarly_paper.definition}%

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

@ -128,14 +128,15 @@ doc_class math_content = tc +
referentiable :: bool <= True
short_name :: string <= "''''"
status :: status <= "semiformal"
mcc :: "math_content_class" <= "lem"
mcc :: "math_content_class" <= "thm"
invariant s1 :: "\<lambda> \<sigma>. \<not>referentiable \<sigma> \<longrightarrow> short_name \<sigma> = ''''"
invariant s2 :: "\<lambda> \<sigma>. status \<sigma> = semiformal"
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
\<^verbatim>\<open>math_example\<close> (or \<^verbatim>\<open>math_ex\<close> for short)
are \<^emph>\<open>informal\<close> descriptions of semi-formal definitions (by inheritance).\<close>
are \<^emph>\<open>informal\<close> descriptions of semi-formal definitions (by inheritance).
Math-Examples can be made referentiable triggering explicit, numbered presentations.\<close>
doc_class math_motivation = tc +
referentiable :: bool <= False
type_synonym math_mtv = math_motivation