forked from Isabelle_DOF/Isabelle_DOF
Merge branch 'master' of logicalhacking.com:HOL-OCL/Isabelle_DOF
This commit is contained in:
commit
25c295dd7f
1
ROOT
1
ROOT
|
@ -8,6 +8,7 @@ session "Isabelle_DOF" = "Functional-Automata" +
|
||||||
"ontologies/CENELEC_50126"
|
"ontologies/CENELEC_50126"
|
||||||
"ontologies/Conceptual"
|
"ontologies/Conceptual"
|
||||||
"ontologies/scholarly_paper"
|
"ontologies/scholarly_paper"
|
||||||
|
"ontologies/technical_report"
|
||||||
"ontologies/mathex_onto"
|
"ontologies/mathex_onto"
|
||||||
|
|
||||||
|
|
||||||
|
|
|
@ -4,7 +4,7 @@ theory MyCommentedIsabelle
|
||||||
begin
|
begin
|
||||||
|
|
||||||
|
|
||||||
open_monitor*[this::article]
|
open_monitor*[this::report]
|
||||||
(*>*)
|
(*>*)
|
||||||
|
|
||||||
title*[tit::title]\<open>An Account with my Personal, Ecclectic Comments on the Isabelle Architecture\<close>
|
title*[tit::title]\<open>An Account with my Personal, Ecclectic Comments on the Isabelle Architecture\<close>
|
||||||
|
|
Binary file not shown.
|
@ -13,8 +13,9 @@ doc_class subtitle =
|
||||||
-- \<open>adding a contribution list and checking that it is cited as well in tech as in conclusion. ? \<close>
|
-- \<open>adding a contribution list and checking that it is cited as well in tech as in conclusion. ? \<close>
|
||||||
|
|
||||||
doc_class author =
|
doc_class author =
|
||||||
email :: "string"
|
email :: "string" <= "''''"
|
||||||
orcid :: "string"
|
http_site :: "string" <= "''''"
|
||||||
|
orcid :: "string" <= "''''"
|
||||||
affiliation :: "string"
|
affiliation :: "string"
|
||||||
|
|
||||||
doc_class abstract =
|
doc_class abstract =
|
||||||
|
|
|
@ -4,8 +4,11 @@ theory technical_report
|
||||||
imports "scholarly_paper"
|
imports "scholarly_paper"
|
||||||
begin
|
begin
|
||||||
|
|
||||||
doc_class table_of_content =
|
doc_class table_of_contents =
|
||||||
level :: int <= 3
|
depth :: int <= 3
|
||||||
|
|
||||||
|
doc_class front_matter =
|
||||||
|
style :: string
|
||||||
|
|
||||||
doc_class "chapter" = text_section +
|
doc_class "chapter" = text_section +
|
||||||
style :: string
|
style :: string
|
||||||
|
@ -16,11 +19,13 @@ doc_class report =
|
||||||
accepts "(title ~~
|
accepts "(title ~~
|
||||||
\<lbrakk>subtitle\<rbrakk> ~~
|
\<lbrakk>subtitle\<rbrakk> ~~
|
||||||
\<lbrace>author\<rbrace>\<^sup>+ ~~
|
\<lbrace>author\<rbrace>\<^sup>+ ~~
|
||||||
|
\<lbrakk>front_matter\<rbrakk> ~~
|
||||||
abstract ~~
|
abstract ~~
|
||||||
chapter ~~
|
\<lbrakk>table_of_contents\<rbrakk> ~~
|
||||||
introduction ~~
|
introduction ~~
|
||||||
\<lbrace>technical || example\<rbrace>\<^sup>+ ~~
|
\<lbrace>technical || example\<rbrace>\<^sup>+ ~~
|
||||||
conclusion ~~
|
conclusion ~~
|
||||||
|
\<lbrakk>table_of_contents\<rbrakk> ~~
|
||||||
bibliography)"
|
bibliography)"
|
||||||
|
|
||||||
end
|
end
|
||||||
|
|
Loading…
Reference in New Issue