Resolved naming inconsistency (mathex_onto vs. math_exam).
Isabelle_DOF/Isabelle_DOF/master There was a failure building this commit Details

This commit is contained in:
Achim D. Brucker 2019-07-20 21:51:55 +01:00
parent 8953f37629
commit 6fd22a071f
7 changed files with 7 additions and 7 deletions

View File

@ -1,6 +1,6 @@
(*<*)
theory MathExam
imports "Isabelle_DOF.mathex"
imports "Isabelle_DOF.math_exam"
HOL.Real
begin
(*>*)

View File

@ -1,2 +1,2 @@
Template: scrartcl
Ontology: mathex
Ontology: math_exam

View File

@ -389,7 +389,7 @@ text\<open> The document class \inlineisar+figure+ --- supported by the \isadof
such as @{docitem_ref \<open>fig_figures\<close>}.
\<close>
subsection*[mathex::example]\<open> The Math-Exam Scenario \<close>
subsection*[math_exam::example]\<open> The Math-Exam Scenario \<close>
text\<open> The Math-Exam Scenario is an application with mixed formal and
semi-formal content. It addresses applications where the author of the exam is not present
during the exam and the preparation requires a very rigorous process, as the french

View File

@ -251,7 +251,7 @@ doc_class srac = ec +
\end{isar}
\<close>
section*[mathex::example]\<open> The Math-Exam Scenario \<close>
section*[math_exam::example]\<open> The Math-Exam Scenario \<close>
text\<open> The Math-Exam Scenario is an application with mixed formal and
semi-formal content. It addresses applications where the author of the exam is not present
during the exam and the preparation requires a very rigorous process, as the french

View File

@ -12,7 +12,7 @@
%% SPDX-License-Identifier: LPPL-1.0+ OR BSD-2-Clause
\NeedsTeXFormat{LaTeX2e}\relax
\ProvidesPackage{DOF-mathex}
\ProvidesPackage{DOF-math_exam}
[0000/00/00 Unreleased v0.0.0+%
Document-Type Support Framework for math classes.]

View File

@ -1,4 +1,4 @@
theory mathex
theory math_exam
imports "../../DOF/Isa_COL"
begin

View File

@ -3,7 +3,7 @@ theory
imports
"CENELEC_50128/CENELEC_50128"
"Conceptual/Conceptual"
"mathex/mathex"
"math_exam/math_exam"
"math_paper/math_paper"
"scholarly_paper/scholarly_paper"
"small_math/small_math"