Isabelle_DOF
/
Isabelle_DOF
1
0
Fork 2
Code Issues 1 Pull Requests Releases Wiki Activity

Revised Sec. 4.1.

This commit is contained in:
Achim D. Brucker 2021-02-09 20:56:56 +00:00
parent 43184a9995
commit 3649fb855e
1 changed files with 11 additions and 13 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

24
examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy
View File

@ -51,13 +51,13 @@ text\<open>
\<close> \<close>
text\<open> text\<open>
Similarly to Isabelle, which is based on a core logic \<^theory>\<open>Pure\<close> and then extended by libraries Similarly to Isabelle, which is based on a core logic \<^theory>\<open>Pure\<close> and then extended by libraries
to major systems like \<^verbatim>\<open>HOL\<close> or \<^verbatim>\<open>FOL\<close>, \<^isadof> has a generic core infrastructure \<^dof> and then to major systems like \<^verbatim>\<open>HOL\<close>, \<^isadof> has a generic core infrastructure \<^dof> and then
presents itself to users via major library extensions, which add domain-specific presents itself to users via major library extensions, which add domain-specific
system-extensions. Consequently, ontologies in \<^isadof> are not just a sequence of descriptions in system-extensions. Ontologies in \<^isadof> are not just a sequence of descriptions in
\<^isadof>'s Ontology Definition Language (ODL). Rather, they are themselves presented as integrated \<^isadof>'s Ontology Definition Language (ODL). Rather, they are themselves presented as integrated
sources that provide textual decriptions, abbreviations, macro-support and even ML-code. sources that provide textual decriptions, abbreviations, macro-support and even ML-code.
Conceptually, the library of \<^isadof> is currently organized as follows Conceptually, the library of \<^isadof> is currently organized as follows\<^footnote>\<open>Note that the \<^emph>\<open>technical\<close>
\<^footnote>\<open>Note that the \<^emph>\<open>technical\<close> organisation is slightly different and shown in organisation is slightly different and shown in
@{technical (unchecked) \<open>infrastructure\<close>}.\<close>: @{technical (unchecked) \<open>infrastructure\<close>}.\<close>:
% %
\begin{center} \begin{center}
@ -114,9 +114,9 @@ text\<open>
\<^emph>\<open>is-a\<close> relation between classes; \<^emph>\<open>is-a\<close> relation between classes;
\<^item> classes may refer to other classes via a regular expression in a \<^item> classes may refer to other classes via a regular expression in a
\<^emph>\<open>where\<close> clause; \<^emph>\<open>where\<close> clause;
(* % TODO: % TODO:
% Update to the new implementation. % Update to the new implementation.
% where is deprecated and the new implementation uses accepts and rejects. *) % where is deprecated and the new implementation uses accepts and rejects.
\<^item> attributes may have default values in order to facilitate notation. \<^item> attributes may have default values in order to facilitate notation.
\<close> \<close>
@ -149,9 +149,9 @@ text\<open>
classes and their inheritance relation structure meta-data of text-elements in an object-oriented classes and their inheritance relation structure meta-data of text-elements in an object-oriented
manner, monitor classes enforce structural organization of documents via the language specified manner, monitor classes enforce structural organization of documents via the language specified
by the regular expression enforcing a sequence of text-elements. by the regular expression enforcing a sequence of text-elements.
(* % TODO: % TODO:
% Update to the new implementation. % Update to the new implementation.
% where is deprecated and the new implementation uses accepts and rejects. *) % where is deprecated and the new implementation uses accepts and rejects.
A major design decision of ODL is to denote attribute values by HOL-terms and HOL-types. A major design decision of ODL is to denote attribute values by HOL-terms and HOL-types.
Consequently, ODL can refer to any predefined type defined in the HOL library, \<^eg>, Consequently, ODL can refer to any predefined type defined in the HOL library, \<^eg>,
@ -177,9 +177,9 @@ text\<open>
in \<^boxed_theory_text>\<open> ... \<close> which might contain certain ``quasi-letters'' such in \<^boxed_theory_text>\<open> ... \<close> which might contain certain ``quasi-letters'' such
as \<^boxed_theory_text>\<open>_\<close>, \<^boxed_theory_text>\<open>-\<close>, \<^boxed_theory_text>\<open>.\<close> (see~@{cite "wenzel:isabelle-isar:2020"} for as \<^boxed_theory_text>\<open>_\<close>, \<^boxed_theory_text>\<open>-\<close>, \<^boxed_theory_text>\<open>.\<close> (see~@{cite "wenzel:isabelle-isar:2020"} for
details). details).
(* % TODO % TODO
% This phrase should be reviewed to clarify identifiers. % This phrase should be reviewed to clarify identifiers.
% Peculiarly, "and identifiers in \<^boxed_theory_text>\<open> ... \<close>". *) % Peculiarly, "and identifiers in \<^boxed_theory_text>\<open> ... \<close>".
\<^item> \<open>tyargs\<close>:\<^index>\<open>tyargs@\<open>tyargs\<close>\<close> \<^item> \<open>tyargs\<close>:\<^index>\<open>tyargs@\<open>tyargs\<close>\<close>
\<^rail>\<open> typefree | ('(' (typefree * ',') ')')\<close> \<^rail>\<open> typefree | ('(' (typefree * ',') ')')\<close>
\<open>typefree\<close> denotes fixed type variable(\<open>'a\<close>, \<open>'b\<close>, ...) (see~@{cite "wenzel:isabelle-isar:2020"}) \<open>typefree\<close> denotes fixed type variable(\<open>'a\<close>, \<open>'b\<close>, ...) (see~@{cite "wenzel:isabelle-isar:2020"})
@ -300,7 +300,7 @@ text\<open>
underscore ``\_'') that do have a special meaning in \<^LaTeX>. underscore ``\_'') that do have a special meaning in \<^LaTeX>.
Moreover, as usual, special care has to be taken for commands that write into aux-files Moreover, as usual, special care has to be taken for commands that write into aux-files
that are included in a following \<^LaTeX>-run. For such complex examples, we refer the interested that are included in a following \<^LaTeX>-run. For such complex examples, we refer the interested
reader, in general, to the style files provided in the \<^isadof> distribution. In particular reader to the style files provided in the \<^isadof> distribution. In particular
the definitions of the concepts \<^boxed_theory_text>\<open>title*\<close> and \<^boxed_theory_text>\<open>author*\<close> in the the definitions of the concepts \<^boxed_theory_text>\<open>title*\<close> and \<^boxed_theory_text>\<open>author*\<close> in the
file \<^file>\<open>../../../src/ontologies/scholarly_paper/DOF-scholarly_paper.sty\<close> show examples of protecting file \<^file>\<open>../../../src/ontologies/scholarly_paper/DOF-scholarly_paper.sty\<close> show examples of protecting
special characters in definitions that need to make use of a entries in an aux-file. special characters in definitions that need to make use of a entries in an aux-file.
@ -371,8 +371,6 @@ For a declared class \<^theory_text>\<open>cid\<close>, there exists a text anti
The precise presentation is decided in the \<^emph>\<open>layout definitions\<close>, for example by suitable The precise presentation is decided in the \<^emph>\<open>layout definitions\<close>, for example by suitable
\<^LaTeX>-template code. Declared but not yet defined instances must be referenced with a particular \<^LaTeX>-template code. Declared but not yet defined instances must be referenced with a particular
pragma in order to enforce a relaxed checking \<^theory_text>\<open> @{cid (unchecked) \<open>oid\<close>} \<close>. pragma in order to enforce a relaxed checking \<^theory_text>\<open> @{cid (unchecked) \<open>oid\<close>} \<close>.
(* % there should also exist a *term* antiquotation ... *)
\<close> \<close>
(*<*) (*<*)