From b91377edbd8ff2d39ef3c821efcb8e5932d352d9 Mon Sep 17 00:00:00 2001 From: "Achim D. Brucker" Date: Sun, 6 Jan 2019 18:22:54 +0000 Subject: [PATCH] Base examples on the session Isabelle_DOF. --- examples/math_exam/BAC2017/BAC2017.thy | 2 +- examples/math_exam/BAC2017/ROOT | 3 +-- examples/math_exam/MathExam/MathExam.thy | 2 +- examples/math_exam/MathExam/ROOT | 5 +---- examples/scholarly_paper/2018_cicm/IsaDofApplications.thy | 2 +- examples/scholarly_paper/2018_cicm/ROOT | 4 +--- examples/technical_report/IsaDof_Manual/00_Frontmatter.thy | 2 +- examples/technical_report/IsaDof_Manual/ROOT | 5 +---- .../TR_my_commented_isabelle/MyCommentedIsabelle.thy | 2 +- examples/technical_report/TR_my_commented_isabelle/ROOT | 5 +---- 10 files changed, 10 insertions(+), 22 deletions(-) diff --git a/examples/math_exam/BAC2017/BAC2017.thy b/examples/math_exam/BAC2017/BAC2017.thy index a4eebb5a..5177fb72 100644 --- a/examples/math_exam/BAC2017/BAC2017.thy +++ b/examples/math_exam/BAC2017/BAC2017.thy @@ -1,5 +1,5 @@ theory BAC2017 - imports "../../../ontologies/mathex_onto" + imports "Isabelle_DOF.mathex_onto" Deriv Transcendental begin diff --git a/examples/math_exam/BAC2017/ROOT b/examples/math_exam/BAC2017/ROOT index 92e909c8..61540428 100644 --- a/examples/math_exam/BAC2017/ROOT +++ b/examples/math_exam/BAC2017/ROOT @@ -1,7 +1,6 @@ -session "BAC2017" = "Functional-Automata" + +session "BAC2017" = "Isabelle_DOF" + options [document = pdf, document_output = "output",quick_and_dirty=true] theories [document = false] - "../../../ontologies/mathex_onto" "Deriv" "Transcendental" theories diff --git a/examples/math_exam/MathExam/MathExam.thy b/examples/math_exam/MathExam/MathExam.thy index 5cc6190f..0c2f8519 100644 --- a/examples/math_exam/MathExam/MathExam.thy +++ b/examples/math_exam/MathExam/MathExam.thy @@ -1,6 +1,6 @@ (*<*) theory MathExam - imports "../../../ontologies/mathex_onto" + imports "Isabelle_DOF.mathex_onto" Real begin (*>*) diff --git a/examples/math_exam/MathExam/ROOT b/examples/math_exam/MathExam/ROOT index 4d4f652c..3474ce43 100644 --- a/examples/math_exam/MathExam/ROOT +++ b/examples/math_exam/MathExam/ROOT @@ -1,8 +1,5 @@ -session "MathExam" = "Functional-Automata" + +session "MathExam" = "Isabelle_DOF" + options [document = pdf, document_output = "output"] - theories [document = false] - (* Foo *) - "../../../ontologies/mathex_onto" theories MathExam document_files diff --git a/examples/scholarly_paper/2018_cicm/IsaDofApplications.thy b/examples/scholarly_paper/2018_cicm/IsaDofApplications.thy index c35ebd72..1c99c083 100644 --- a/examples/scholarly_paper/2018_cicm/IsaDofApplications.thy +++ b/examples/scholarly_paper/2018_cicm/IsaDofApplications.thy @@ -1,6 +1,6 @@ (*<*) theory IsaDofApplications - imports "../../../ontologies/scholarly_paper" + imports "Isabelle_DOF.scholarly_paper" begin open_monitor*[this::article] diff --git a/examples/scholarly_paper/2018_cicm/ROOT b/examples/scholarly_paper/2018_cicm/ROOT index eaf658c6..fac0be9a 100644 --- a/examples/scholarly_paper/2018_cicm/ROOT +++ b/examples/scholarly_paper/2018_cicm/ROOT @@ -1,7 +1,5 @@ -session "IsaDofApplications" = "Functional-Automata" + +session "IsaDofApplications" = "Isabelle_DOF" + options [document = pdf, document_output = "output", quick_and_dirty = true] - theories [document = false] - "../../../ontologies/scholarly_paper" theories IsaDofApplications document_files diff --git a/examples/technical_report/IsaDof_Manual/00_Frontmatter.thy b/examples/technical_report/IsaDof_Manual/00_Frontmatter.thy index 4af325e5..6fe0f146 100644 --- a/examples/technical_report/IsaDof_Manual/00_Frontmatter.thy +++ b/examples/technical_report/IsaDof_Manual/00_Frontmatter.thy @@ -1,6 +1,6 @@ (*<*) theory "00_Frontmatter" - imports "../../../ontologies/technical_report" + imports "Isabelle_DOF.technical_report" begin open_monitor*[this::report] diff --git a/examples/technical_report/IsaDof_Manual/ROOT b/examples/technical_report/IsaDof_Manual/ROOT index c57b2b87..1a0b5fd8 100644 --- a/examples/technical_report/IsaDof_Manual/ROOT +++ b/examples/technical_report/IsaDof_Manual/ROOT @@ -1,8 +1,5 @@ -session "IsaDof_Manual" = "Functional-Automata" + +session "IsaDof_Manual" = "Isabelle_DOF" + options [document = pdf, document_output = "output", quick_and_dirty = true] - theories [document = false] - "../../../ontologies/scholarly_paper" - "../../../ontologies/technical_report" theories IsaDofManual document_files diff --git a/examples/technical_report/TR_my_commented_isabelle/MyCommentedIsabelle.thy b/examples/technical_report/TR_my_commented_isabelle/MyCommentedIsabelle.thy index 626b74d7..21a207a9 100644 --- a/examples/technical_report/TR_my_commented_isabelle/MyCommentedIsabelle.thy +++ b/examples/technical_report/TR_my_commented_isabelle/MyCommentedIsabelle.thy @@ -1,6 +1,6 @@ (*<*) theory MyCommentedIsabelle - imports "../../../ontologies/technical_report" + imports "Isabelle_DOF.technical_report" begin diff --git a/examples/technical_report/TR_my_commented_isabelle/ROOT b/examples/technical_report/TR_my_commented_isabelle/ROOT index 800b9c7e..e992146a 100644 --- a/examples/technical_report/TR_my_commented_isabelle/ROOT +++ b/examples/technical_report/TR_my_commented_isabelle/ROOT @@ -1,8 +1,5 @@ -session "TR_mycommentedisabelle" = "Functional-Automata" + +session "TR_mycommentedisabelle" = "Isabelle_DOF" + options [document = pdf, document_output = "output",quick_and_dirty = true] - theories [document = false] - "../../../ontologies/scholarly_paper" - "../../../ontologies/technical_report" theories "MyCommentedIsabelle" document_files