forked from Isabelle_DOF/Isabelle_DOF
New LaTeX chapter introduced. Structuring proposal
This commit is contained in:
parent
62cf2264a2
commit
a28ceb98eb
|
@ -52,14 +52,14 @@ framework in the style of~@{cite "wenzel.ea:building:2007"}.
|
||||||
(*<*)
|
(*<*)
|
||||||
declare_reference*[bgrnd::text_section]
|
declare_reference*[bgrnd::text_section]
|
||||||
declare_reference*[isadof::text_section]
|
declare_reference*[isadof::text_section]
|
||||||
declare_reference*[ontomod::text_section]
|
declare_reference*[casestudies::text_section]
|
||||||
declare_reference*[ontopide::text_section]
|
declare_reference*[ontopide::text_section]
|
||||||
declare_reference*[conclusion::text_section]
|
declare_reference*[conclusion::text_section]
|
||||||
(*>*)
|
(*>*)
|
||||||
text*[plan::introduction]\<open> The plan of the paper is follows: we start by introducing the underlying
|
text*[plan::introduction]\<open> The plan of the paper is follows: we start by introducing the underlying
|
||||||
Isabelel sytem (@{docitem_ref (unchecked) \<open>bgrnd\<close>}) followed by presenting the
|
Isabelle sytem (@{docitem_ref (unchecked) \<open>bgrnd\<close>}) followed by presenting the
|
||||||
essentials of \isadof and its ontology language (@{docitem_ref (unchecked) \<open>isadof\<close>}).
|
essentials of \isadof and its ontology language (@{docitem_ref (unchecked) \<open>isadof\<close>}).
|
||||||
It follows @{docitem_ref (unchecked) \<open>ontomod\<close>}, where we present three application
|
It follows @{docitem_ref (unchecked) \<open>casestudies\<close>}, where we present three application
|
||||||
scenarios from the point of view of the ontology modeling. In @{docitem_ref (unchecked) \<open>ontopide\<close>}
|
scenarios from the point of view of the ontology modeling. In @{docitem_ref (unchecked) \<open>ontopide\<close>}
|
||||||
we discuss the user-interaction generated from the ontological definitions. Finally, we draw
|
we discuss the user-interaction generated from the ontological definitions. Finally, we draw
|
||||||
conclusions and discuss related work in @{docitem_ref (unchecked) \<open>conclusion\<close>}. \<close>
|
conclusions and discuss related work in @{docitem_ref (unchecked) \<open>conclusion\<close>}. \<close>
|
||||||
|
|
|
@ -4,7 +4,8 @@ theory "03_IsaDof"
|
||||||
begin
|
begin
|
||||||
(*>*)
|
(*>*)
|
||||||
|
|
||||||
chapter*[isadof::technical,main_author="Some(@{docitem ''adb''}::author)"]\<open> \isadof \<close>
|
chapter*[isadof::technical,main_author="Some(@{docitem ''adb''}::author)"]
|
||||||
|
\<open> \isadof : Design and Use of its Commands\<close>
|
||||||
|
|
||||||
text\<open> An \isadof document consists of three components:
|
text\<open> An \isadof document consists of three components:
|
||||||
\<^item> the \<^emph>\<open>ontology definition\<close> which is an Isabelle theory file with definitions
|
\<^item> the \<^emph>\<open>ontology definition\<close> which is an Isabelle theory file with definitions
|
||||||
|
|
|
@ -0,0 +1,16 @@
|
||||||
|
(*<*)
|
||||||
|
theory "05_IsaDofLaTeX"
|
||||||
|
imports "04_IsaDofCaseStudies"
|
||||||
|
begin
|
||||||
|
(*>*)
|
||||||
|
|
||||||
|
chapter*[latex::example,main_author="Some(@{docitem ''adb''}::author)"]\<open> PDF Generation with \isadof \<close>
|
||||||
|
|
||||||
|
text\<open> ...\<close>
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
(*<*)
|
||||||
|
end
|
||||||
|
(*>*)
|
||||||
|
|
|
@ -1,7 +1,6 @@
|
||||||
(*<*)
|
(*<*)
|
||||||
theory "06_Conclusion"
|
theory "06_Conclusion"
|
||||||
imports "04_IsaDofCaseStudies"
|
imports "05_IsaDofLaTeX"
|
||||||
(* imports "05_DesignImpl *)
|
|
||||||
begin
|
begin
|
||||||
(*>*)
|
(*>*)
|
||||||
|
|
||||||
|
|
|
@ -10,6 +10,8 @@ text*[bib::bibliography]\<open>References\<close>
|
||||||
|
|
||||||
close_monitor*[this]
|
close_monitor*[this]
|
||||||
|
|
||||||
|
check_doc_global
|
||||||
|
|
||||||
text\<open>Resulting trace in doc\_item ''this'': \<close>
|
text\<open>Resulting trace in doc\_item ''this'': \<close>
|
||||||
ML\<open>@{trace_attribute this}\<close>
|
ML\<open>@{trace_attribute this}\<close>
|
||||||
|
|
||||||
|
|
File diff suppressed because it is too large
Load Diff
Reference in New Issue