Removed relative imports in all non-trivial examples.
Isabelle_DOF/Isabelle_DOF/master This commit looks good Details

This commit is contained in:
Achim D. Brucker 2019-07-12 20:20:02 +01:00
parent 9c21b7a89a
commit 6a1af31529
4 changed files with 8 additions and 9 deletions

View File

@ -1,8 +1,9 @@
chapter\<open> Example : Forward and Standard (use-after-define) Referencing\<close>
theory Example
imports "../../ontologies/CENELEC_50128"
"../../ontologies/scholarly_paper"
imports
Isabelle_DOF.CENELEC_50128
Isabelle_DOF.scholarly_paper
begin
section\<open> Some examples of Isabelle's standard antiquotations. \<close>
@ -101,4 +102,4 @@ text\<open>The recurring issue of the certification
end

View File

@ -1,7 +1,6 @@
(*<*)
theory "00_Frontmatter"
(* imports "Isabelle_DOF.technical_report" *)
imports "../../../ontologies/technical_report"
imports "Isabelle_DOF.technical_report"
begin
open_monitor*[this::report]

View File

@ -152,11 +152,11 @@ particular document into the context of our conceptual example
ontology shown above:
\begin{isar}
theory Concept_Example
imports "../../ontologies/Conceptual"
imports Isabelle_DOF.Conceptual
begin
\end{isar}
which is contained contained a theory file
\verb+../../ontologies/Conceptual.thy+. Then we can continue to annotate
\verb+ontologies/Conceptual.thy+ in the \isadof distribution. Then we can continue to annotate
our text as follows:
\begin{isar}
section*[a::A, x = "''alpha''"] {* Lorem ipsum dolor sit amet, ... *}
@ -322,7 +322,7 @@ monitors may be nested.
text\<open>
\begin{isar}[float, caption={Our running example},label={lst:example}]
theory Concept_Example
imports "../../ontologies/Conceptual"
imports "Isabelle_DOF.Conceptual"
begin
open_monitor*[struct::M]

View File

@ -1,7 +1,6 @@
(*<*)
theory MyCommentedIsabelle
imports "Isabelle_DOF.technical_report"
(*imports "../../../ontologies/technical_report"*)
begin