From 14d03320b60342dd853f56f21a8a1acdfaf6f11f Mon Sep 17 00:00:00 2001 From: bu Date: Tue, 20 Mar 2018 22:28:23 +0100 Subject: [PATCH] Neues Beispiel und Kleinkram. --- LNCS_onto.thy | 48 ++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 48 insertions(+) create mode 100644 LNCS_onto.thy diff --git a/LNCS_onto.thy b/LNCS_onto.thy new file mode 100644 index 0000000..c61a8c0 --- /dev/null +++ b/LNCS_onto.thy @@ -0,0 +1,48 @@ +theory LNCS_onto + imports Isa_DOF +begin + +doc_class title = + short_title :: "string option" -- None + +doc_class subtitle = + abbrev :: "string option" -- None + +doc_class author = + affiliation :: "string" + +doc_class abstract = + keywds :: "string list" + +doc_class introduction = + main_author :: "author option" + +doc_class tech_section = + main_author :: "author option" + +doc_class conclusion = + main_author :: "author option" + +doc_class bibliography = + style :: "string option" -- "''LNCS''" + +doc_class article = + T :: "title option" -- None + ST :: "subtitle option" -- None + AS :: "author list" + ABS :: "abstract option" + INTRO :: "introduction option" + TS :: "tech_section list" + CON :: "conclusion" + where "(title . + [subtitle] . + (author)+ . + abstract . + introduction . + (tech_section)+ . + conclusion . + bibliography)" + + +end +