From 7e01ff70216645864270c3d78a18d4b7ead2a9a3 Mon Sep 17 00:00:00 2001 From: "Achim D. Brucker" Date: Fri, 8 Jan 2021 03:54:37 +0000 Subject: [PATCH] Cleanup. --- .../Isabelle_DOF-Manual/02_Background.thy | 44 +++++-------------- .../document/lstisadof-manual.sty | 5 ++- .../Isabelle_DOF-Manual/document/preamble.tex | 1 + 3 files changed, 14 insertions(+), 36 deletions(-) diff --git a/examples/technical_report/Isabelle_DOF-Manual/02_Background.thy b/examples/technical_report/Isabelle_DOF-Manual/02_Background.thy index 31119026..9ef95920 100755 --- a/examples/technical_report/Isabelle_DOF-Manual/02_Background.thy +++ b/examples/technical_report/Isabelle_DOF-Manual/02_Background.thy @@ -1,7 +1,7 @@ (************************************************************************* * Copyright (C) - * 2019-2020 The University of Exeter - * 2018-2020 The University of Paris-Saclay + * 2019-2021 The University of Exeter + * 2018-2021 The University of Paris-Saclay * 2018 The University of Sheffield * * License: @@ -85,26 +85,20 @@ text\ imports (* Declaration of 'theory' dependencies *) Main (* Imports a library called 'Main' *) keywords (* Registration of keywords defined locally *) - requirement (* A command for describing requirements *) -\} + requirement (* A command for describing requirements *)\} where \<^boxed_theory_text>\Example\ is the abstract name of the text-file, \<^boxed_theory_text>\Main\ refers to an imported theory (recall that the import relation must be acyclic) and \<^boxed_theory_text>\keywords\ are used to separate commands from each other. \ -(* experiment starts here *) -(* somewhere we destroyed the standard antiquotation thm ... -text\ \<^emph>\blabla\ @{thm \refl\}\ -text\ According to the \<^emph>\reflexivity\ axiom @{thm refl}, we obtain in \ - for @{term "fac 5"} the result @{value "fac 5"}.\ -*) text\ A text-element \<^index>\text-element\ may look like this: - \<^theory_text>\text\ According to the *\reflexivity\ axiom @{thm refl}, we obtain in \ - for @{term "fac 5"} the result @{value "fac 5"}.\\ + @{boxed_theory_text [display]\ +text\ According to the \<^emph>\reflexivity\ axiom @{thm refl}, + we obtain in \ for @{term "fac 5"} the result @{value "fac 5"}.\\} so it is a command \<^theory_text>\text\ followed by an argument (here in \\ ... \\ paranthesis) which contains characters and and a special notation for semantic macros \<^bindex>\semantic macros\ -(here in the notation\<^theory_text>\@{term "fac 5"}).\ +(here in the notation \<^theory_text>\@{term "fac 5"}).\ \ text\ @@ -121,35 +115,17 @@ text\ This document model can be instantiated with outer-syntax commands for common text elements, \<^eg>, \<^theory_text>\section\...\\ or \<^theory_text>\text\...\\. Thus, users can add informal text to a sub-document using a text command: - @{boxed_theory_text [display] \text\This is a description.\\ } - - @{boxed_theory_text [display]\ - text\This is a description.\ - \} This will type-set the corresponding text in, for example, a PDF document. However, this translation is not necessarily one-to-one: text elements can be enriched by formal, \<^ie>, - machine-checked content via *\semantic macros\, called antiquotations\<^bindex>\antiquotation\: - + machine-checked content via \<^emph>\semantic macros\, called antiquotations\<^bindex>\antiquotation\: @{boxed_theory_text [display] - \text\ According to the *\reflexivity\ axiom @{thm refl}, we obtain in \ + \text\ According to the \<^emph>\reflexivity\ axiom @{thm refl}, we obtain in \ for @{term "fac 5"} the result @{value "fac 5"}.\\ } - -@{boxed_theory_text [display]\ -text\According to the *\reflexivity\ axiom <@>{thm refl}, we obtain in \ - for @{term "fac 5"} the result @{value "fac 5"}.\ -\} - - which is represented in the final document (\<^eg>, a PDF) by: -\begin{out} -According to the \emph{reflexivity} axiom $\mathrm{x = x}$, we obtain in $\Gamma$ -for $\operatorname{fac} \text{\textrm{5}}$ the result $\text{\textrm{120}}$. -\end{out} - @{boxed_pdf [display] -\According to the \emph{reflexivity} axiom $\mathrm{x = x}$, we obtain in $\Gamma$ +\According to the $\emph{reflexivity}$ axiom $\mathrm{x = x}$, we obtain in $\Gamma$ for $\operatorname{fac} \text{\textrm{5}}$ the result $\text{\textrm{120}}$.\ } diff --git a/examples/technical_report/Isabelle_DOF-Manual/document/lstisadof-manual.sty b/examples/technical_report/Isabelle_DOF-Manual/document/lstisadof-manual.sty index a25e2ae7..d81005e3 100755 --- a/examples/technical_report/Isabelle_DOF-Manual/document/lstisadof-manual.sty +++ b/examples/technical_report/Isabelle_DOF-Manual/document/lstisadof-manual.sty @@ -1,6 +1,6 @@ %% Copyright (C) 2018 The University of Sheffield -%% 2018 The University of Paris-Saclay -%% 2019 The University of Exeter +%% 2018-2021 The University of Paris-Saclay +%% 2019-2021 The University of Exeter %% %% License: %% This program can be redistributed and/or modified under the terms @@ -90,6 +90,7 @@ ,enhanced jigsaw ,borderline west={2pt}{0pt}{isar!60!black} ,sharp corners + ,before skip balanced=0.5\baselineskip plus 2pt % ,before skip=10pt % ,after skip=10pt ,enlarge top by=0mm diff --git a/examples/technical_report/Isabelle_DOF-Manual/document/preamble.tex b/examples/technical_report/Isabelle_DOF-Manual/document/preamble.tex index 1b458f38..1c0b6f06 100755 --- a/examples/technical_report/Isabelle_DOF-Manual/document/preamble.tex +++ b/examples/technical_report/Isabelle_DOF-Manual/document/preamble.tex @@ -30,6 +30,7 @@ %\AtEndDocument{\printindex} \newcommand{\dof}{DOF\xspace} +\newcommand{\isactrlemph}{*} \newcommand{\path}[1]{\texttt{\nolinkurl{#1}}} \title{}