diff --git a/examples/math_exam/MathExam/MathExam.thy b/examples/math_exam/MathExam/MathExam.thy index 9772699..0699adf 100644 --- a/examples/math_exam/MathExam/MathExam.thy +++ b/examples/math_exam/MathExam/MathExam.thy @@ -1,6 +1,6 @@ (*<*) theory MathExam - imports "Isabelle_DOF.mathex" + imports "Isabelle_DOF.math_exam" HOL.Real begin (*>*) diff --git a/examples/math_exam/MathExam/document/isadof.cfg b/examples/math_exam/MathExam/document/isadof.cfg index f13f22b..3516c38 100644 --- a/examples/math_exam/MathExam/document/isadof.cfg +++ b/examples/math_exam/MathExam/document/isadof.cfg @@ -1,2 +1,2 @@ Template: scrartcl -Ontology: mathex +Ontology: math_exam diff --git a/examples/scholarly_paper/2018_cicm/IsaDofApplications.thy b/examples/scholarly_paper/2018_cicm/IsaDofApplications.thy index e03b56a..a9d7f65 100644 --- a/examples/scholarly_paper/2018_cicm/IsaDofApplications.thy +++ b/examples/scholarly_paper/2018_cicm/IsaDofApplications.thy @@ -389,7 +389,7 @@ text\ The document class \inlineisar+figure+ --- supported by the \isadof such as @{docitem_ref \fig_figures\}. \ -subsection*[mathex::example]\ The Math-Exam Scenario \ +subsection*[math_exam::example]\ The Math-Exam Scenario \ text\ 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 diff --git a/examples/technical_report/IsaDof_Manual/03_GuidedTour.thy b/examples/technical_report/IsaDof_Manual/03_GuidedTour.thy index e5587aa..8c98821 100644 --- a/examples/technical_report/IsaDof_Manual/03_GuidedTour.thy +++ b/examples/technical_report/IsaDof_Manual/03_GuidedTour.thy @@ -251,7 +251,7 @@ doc_class srac = ec + \end{isar} \ -section*[mathex::example]\ The Math-Exam Scenario \ +section*[math_exam::example]\ The Math-Exam Scenario \ text\ 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 diff --git a/src/ontologies/mathex/DOF-mathex.sty b/src/ontologies/math_exam/DOF-math_exam.sty similarity index 98% rename from src/ontologies/mathex/DOF-mathex.sty rename to src/ontologies/math_exam/DOF-math_exam.sty index 48b0b85..1212629 100644 --- a/src/ontologies/mathex/DOF-mathex.sty +++ b/src/ontologies/math_exam/DOF-math_exam.sty @@ -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.] diff --git a/src/ontologies/mathex/mathex.thy b/src/ontologies/math_exam/math_exam.thy similarity index 99% rename from src/ontologies/mathex/mathex.thy rename to src/ontologies/math_exam/math_exam.thy index fc938dd..be32c2a 100644 --- a/src/ontologies/mathex/mathex.thy +++ b/src/ontologies/math_exam/math_exam.thy @@ -1,4 +1,4 @@ -theory mathex +theory math_exam imports "../../DOF/Isa_COL" begin diff --git a/src/ontologies/ontologies.thy b/src/ontologies/ontologies.thy index aede5e8..7cc6ee4 100644 --- a/src/ontologies/ontologies.thy +++ b/src/ontologies/ontologies.thy @@ -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"