From a79a3f539df218cc2e103e2a0720de913a5ef85f Mon Sep 17 00:00:00 2001 From: "Achim D. Brucker" Date: Thu, 29 Feb 2024 17:36:08 +0000 Subject: [PATCH] Added basic author and title information. --- .../template-beamer-UNSUPPORTED.thy | 61 ++++++++++++++++++- .../template-beamerposter-UNSUPPORTED.thy | 8 +++ .../template-lipics-v2021-UNSUPPORTED.thy | 8 +++ .../template-lncs/template-lncs.thy | 8 +++ .../template-scrartcl/template-scrartcl.thy | 8 +++ .../template-scrreprt-modern.thy | 8 +++ .../template-scrreprt/template-scrreprt.thy | 8 +++ .../template-sn-article-UNSUPPORTED.thy | 8 +++ .../template-svjour3-UNSUPPORTED.thy | 8 +++ 9 files changed, 124 insertions(+), 1 deletion(-) diff --git a/Isabelle_DOF-Examples-Templates/template-beamer-UNSUPPORTED/template-beamer-UNSUPPORTED.thy b/Isabelle_DOF-Examples-Templates/template-beamer-UNSUPPORTED/template-beamer-UNSUPPORTED.thy index 5f45b78..a95919a 100644 --- a/Isabelle_DOF-Examples-Templates/template-beamer-UNSUPPORTED/template-beamer-UNSUPPORTED.thy +++ b/Isabelle_DOF-Examples-Templates/template-beamer-UNSUPPORTED/template-beamer-UNSUPPORTED.thy @@ -1,3 +1,4 @@ +(*<*) theory "template-beamer-UNSUPPORTED" imports @@ -9,5 +10,63 @@ list_templates use_template "beamer-UNSUPPORTED" list_ontologies use_ontology "scholarly_paper" +(*>*) -end +title* [tit::title]\Formal Verification of Security Protocols\ +author*[alice, email = "\alice@example.com\", + affiliation = "\Wonderland University\"]\Alice\ +(* +author*[bob, email = "\bob@example.com\", + affiliation = "\Wonderland University\"]\Bob\ +*) + +text\ +\begin{frame} +\frametitle{Example Slide} +\centering\huge This is an example! +\end{frame} +\ + + +frame*[test_frame + , frametitle = \\\Example Slide\<^sub>t\<^sub>e\<^sub>s\<^sub>t\ with items @{thm "HOL.refl"}\\ + , framesubtitle = "''Subtitle''"] +\This is an example! + \<^item> The term \<^term>\refl\ is... + \<^item> and the term encoding the title of this frame is \<^term_>\frametitle @{frame \test_frame\}\\ + +frame*[test_frame2 + , frametitle = "''Example Slide''" + , framesubtitle = \\\Subtitle\<^sub>t\<^sub>e\<^sub>s\<^sub>t:\ the value of \<^term>\(3::int) + 3\ is @{value "(3::int) + 3"}\\] +\Test frame env \<^term>\refl\\ + +frame*[test_frame3 + , options = "''allowframebreaks''" + , frametitle = "''Example Slide with frame break''" + , framesubtitle = \\\Subtitle\<^sub>t\<^sub>e\<^sub>s\<^sub>t:\ the value of \<^term>\(3::int) + 3\ is @{value "(3::int) + 3"}\\] +\ + \<^item> The term \<^term>\refl\ is... + \<^item> and the term encoding the title of this frame is \<^term_>\frametitle @{frame \test_frame3\}\ + \<^item> The term \<^term>\refl\ is... + \<^item> The term \<^term>\refl\ is... + \<^item> The term \<^term>\refl\ is... + \<^item> The term \<^term>\refl\ is... + \<^item> The term \<^term>\refl\ is... + \<^item> The term \<^term>\refl\ is... + \<^item> The term \<^term>\refl\ is... + \<^item> The term \<^term>\refl\ is... + \<^item> The term \<^term>\refl\ is... + \<^item> The term \<^term>\refl\ is... + \<^item> The term \<^term>\refl\ is... + \<^item> The term \<^term>\refl\ is... + \<^item> The term \<^term>\refl\ is... + \<^item> The term \<^term>\refl\ is... + \<^item> The term \<^term>\refl\ is... + \<^item> The term \<^term>\refl\ is... + \<^item> The term \<^term>\refl\ is... + \<^item> The term \<^term>\refl\ is... +\ + +(*<*) +end +(*>*) diff --git a/Isabelle_DOF-Examples-Templates/template-beamerposter-UNSUPPORTED/template-beamerposter-UNSUPPORTED.thy b/Isabelle_DOF-Examples-Templates/template-beamerposter-UNSUPPORTED/template-beamerposter-UNSUPPORTED.thy index bbb0c7b..e0e77a7 100644 --- a/Isabelle_DOF-Examples-Templates/template-beamerposter-UNSUPPORTED/template-beamerposter-UNSUPPORTED.thy +++ b/Isabelle_DOF-Examples-Templates/template-beamerposter-UNSUPPORTED/template-beamerposter-UNSUPPORTED.thy @@ -10,4 +10,12 @@ use_template "beamerposter-UNSUPPORTED" list_ontologies use_ontology "scholarly_paper" +title* [tit::title]\Formal Verification of Security Protocols\ +author*[alice, email = "\alice@example.com\", + http_site = "\https://example.com/alice\", + affiliation = "\Wonderland University\"]\Alice\ +author*[bob, email = "\bob@example.com\", + http_site = "\https://example.com/bob\", + affiliation = "\Wonderland University\"]\Bob\ + end diff --git a/Isabelle_DOF-Examples-Templates/template-lipics-v2021-UNSUPPORTED/template-lipics-v2021-UNSUPPORTED.thy b/Isabelle_DOF-Examples-Templates/template-lipics-v2021-UNSUPPORTED/template-lipics-v2021-UNSUPPORTED.thy index 5d8ba33..da3d6e3 100644 --- a/Isabelle_DOF-Examples-Templates/template-lipics-v2021-UNSUPPORTED/template-lipics-v2021-UNSUPPORTED.thy +++ b/Isabelle_DOF-Examples-Templates/template-lipics-v2021-UNSUPPORTED/template-lipics-v2021-UNSUPPORTED.thy @@ -10,4 +10,12 @@ use_template "lipics-v2021-UNSUPPORTED" list_ontologies use_ontology "scholarly_paper" +title* [tit::title]\Formal Verification of Security Protocols\ +author*[alice, email = "\alice@example.com\", + http_site = "\https://example.com/alice\", + affiliation = "\Wonderland University\"]\Alice\ +author*[bob, email = "\bob@example.com\", + http_site = "\https://example.com/bob\", + affiliation = "\Wonderland University\"]\Bob\ + end diff --git a/Isabelle_DOF-Examples-Templates/template-lncs/template-lncs.thy b/Isabelle_DOF-Examples-Templates/template-lncs/template-lncs.thy index c506744..f79f67f 100644 --- a/Isabelle_DOF-Examples-Templates/template-lncs/template-lncs.thy +++ b/Isabelle_DOF-Examples-Templates/template-lncs/template-lncs.thy @@ -10,4 +10,12 @@ use_template "lncs" list_ontologies use_ontology "scholarly_paper" +title* [tit::title]\Formal Verification of Security Protocols\ +author*[alice, email = "\alice@example.com\", + http_site = "\https://example.com/alice\", + affiliation = "\Wonderland University\"]\Alice\ +author*[bob, email = "\bob@example.com\", + http_site = "\https://example.com/bob\", + affiliation = "\Wonderland University\"]\Bob\ + end diff --git a/Isabelle_DOF-Examples-Templates/template-scrartcl/template-scrartcl.thy b/Isabelle_DOF-Examples-Templates/template-scrartcl/template-scrartcl.thy index fedd844..f1cf03d 100644 --- a/Isabelle_DOF-Examples-Templates/template-scrartcl/template-scrartcl.thy +++ b/Isabelle_DOF-Examples-Templates/template-scrartcl/template-scrartcl.thy @@ -10,4 +10,12 @@ use_template "scrartcl" list_ontologies use_ontology "scholarly_paper" +title* [tit::title]\Formal Verification of Security Protocols\ +author*[alice, email = "\alice@example.com\", + http_site = "\https://example.com/alice\", + affiliation = "\Wonderland University\"]\Alice\ +author*[bob, email = "\bob@example.com\", + http_site = "\https://example.com/bob\", + affiliation = "\Wonderland University\"]\Bob\ + end diff --git a/Isabelle_DOF-Examples-Templates/template-scrreprt-modern/template-scrreprt-modern.thy b/Isabelle_DOF-Examples-Templates/template-scrreprt-modern/template-scrreprt-modern.thy index ed4fe5f..1bec61e 100644 --- a/Isabelle_DOF-Examples-Templates/template-scrreprt-modern/template-scrreprt-modern.thy +++ b/Isabelle_DOF-Examples-Templates/template-scrreprt-modern/template-scrreprt-modern.thy @@ -10,4 +10,12 @@ use_template "scrreprt-modern" list_ontologies use_ontology "technical_report" +title* [tit::title]\Formal Verification of Security Protocols\ +author*[alice, email = "\alice@example.com\", + http_site = "\https://example.com/alice\", + affiliation = "\Wonderland University\"]\Alice\ +author*[bob, email = "\bob@example.com\", + http_site = "\https://example.com/bob\", + affiliation = "\Wonderland University\"]\Bob\ + end diff --git a/Isabelle_DOF-Examples-Templates/template-scrreprt/template-scrreprt.thy b/Isabelle_DOF-Examples-Templates/template-scrreprt/template-scrreprt.thy index 63a8f2d..73bf685 100644 --- a/Isabelle_DOF-Examples-Templates/template-scrreprt/template-scrreprt.thy +++ b/Isabelle_DOF-Examples-Templates/template-scrreprt/template-scrreprt.thy @@ -10,4 +10,12 @@ use_template "scrreprt" list_ontologies use_ontology "technical_report" +title* [tit::title]\Formal Verification of Security Protocols\ +author*[alice, email = "\alice@example.com\", + http_site = "\https://example.com/alice\", + affiliation = "\Wonderland University\"]\Alice\ +author*[bob, email = "\bob@example.com\", + http_site = "\https://example.com/bob\", + affiliation = "\Wonderland University\"]\Bob\ + end diff --git a/Isabelle_DOF-Examples-Templates/template-sn-article-UNSUPPORTED/template-sn-article-UNSUPPORTED.thy b/Isabelle_DOF-Examples-Templates/template-sn-article-UNSUPPORTED/template-sn-article-UNSUPPORTED.thy index 241ad0a..a41075a 100644 --- a/Isabelle_DOF-Examples-Templates/template-sn-article-UNSUPPORTED/template-sn-article-UNSUPPORTED.thy +++ b/Isabelle_DOF-Examples-Templates/template-sn-article-UNSUPPORTED/template-sn-article-UNSUPPORTED.thy @@ -10,4 +10,12 @@ use_template "sn-article-UNSUPPORTED" list_ontologies use_ontology "scholarly_paper" +title* [tit::title]\Formal Verification of Security Protocols\ +author*[alice, email = "\alice@example.com\", + http_site = "\https://example.com/alice\", + affiliation = "\Wonderland University\"]\Alice\ +author*[bob, email = "\bob@example.com\", + http_site = "\https://example.com/bob\", + affiliation = "\Wonderland University\"]\Bob\ + end diff --git a/Isabelle_DOF-Examples-Templates/template-svjour3-UNSUPPORTED/template-svjour3-UNSUPPORTED.thy b/Isabelle_DOF-Examples-Templates/template-svjour3-UNSUPPORTED/template-svjour3-UNSUPPORTED.thy index e764327..0c50499 100644 --- a/Isabelle_DOF-Examples-Templates/template-svjour3-UNSUPPORTED/template-svjour3-UNSUPPORTED.thy +++ b/Isabelle_DOF-Examples-Templates/template-svjour3-UNSUPPORTED/template-svjour3-UNSUPPORTED.thy @@ -10,4 +10,12 @@ use_template "svjour3-UNSUPPORTED" list_ontologies use_ontology "scholarly_paper" +title* [tit::title]\Formal Verification of Security Protocols\ +author*[alice, email = "\alice@example.com\", + http_site = "\https://example.com/alice\", + affiliation = "\Wonderland University\"]\Alice\ +author*[bob, email = "\bob@example.com\", + http_site = "\https://example.com/bob\", + affiliation = "\Wonderland University\"]\Bob\ + end