diff --git a/examples/cenelec/Example.thy b/examples/cenelec/Example.thy index e4eff0d8..07a8d3f2 100644 --- a/examples/cenelec/Example.thy +++ b/examples/cenelec/Example.thy @@ -1,8 +1,9 @@ chapter\ Example : Forward and Standard (use-after-define) Referencing\ theory Example - imports "../../ontologies/CENELEC_50128" - "../../ontologies/scholarly_paper" + imports + Isabelle_DOF.CENELEC_50128 + Isabelle_DOF.scholarly_paper begin section\ Some examples of Isabelle's standard antiquotations. \ @@ -101,4 +102,4 @@ text\The recurring issue of the certification end - \ No newline at end of file + diff --git a/examples/technical_report/IsaDof_Manual/00_Frontmatter.thy b/examples/technical_report/IsaDof_Manual/00_Frontmatter.thy index 362a3600..6fe0f146 100644 --- a/examples/technical_report/IsaDof_Manual/00_Frontmatter.thy +++ b/examples/technical_report/IsaDof_Manual/00_Frontmatter.thy @@ -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] diff --git a/examples/technical_report/IsaDof_Manual/05_DesignImpl.thy b/examples/technical_report/IsaDof_Manual/05_DesignImpl.thy index f67a1e1f..c183f4cf 100644 --- a/examples/technical_report/IsaDof_Manual/05_DesignImpl.thy +++ b/examples/technical_report/IsaDof_Manual/05_DesignImpl.thy @@ -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\ \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] diff --git a/examples/technical_report/TR_my_commented_isabelle/MyCommentedIsabelle.thy b/examples/technical_report/TR_my_commented_isabelle/MyCommentedIsabelle.thy index 60e2d122..e4652768 100644 --- a/examples/technical_report/TR_my_commented_isabelle/MyCommentedIsabelle.thy +++ b/examples/technical_report/TR_my_commented_isabelle/MyCommentedIsabelle.thy @@ -1,7 +1,6 @@ (*<*) theory MyCommentedIsabelle imports "Isabelle_DOF.technical_report" - (*imports "../../../ontologies/technical_report"*) begin