forked from Isabelle_DOF/Isabelle_DOF
Ad hoc conversion: \begin{isar}...\end{isar} -> @{boxed_theory_text [display] ... }.
This commit is contained in:
parent
6c2ad62df2
commit
109802a76a
|
|
@ -88,10 +88,10 @@ text\<open>
|
|||
\<^item> a light-blue background for input written in Isabelle's Isar language, \<^eg>:
|
||||
|
||||
|
||||
\begin{isar}
|
||||
@{boxed_theory_text [display]\<open>
|
||||
lemma refl: "x = x"
|
||||
by simp
|
||||
\end{isar}
|
||||
\<close>}
|
||||
|
||||
% @ {boxed_isar [display]
|
||||
% \<open>lemma refl: "x = x"
|
||||
|
|
|
|||
|
|
@ -80,13 +80,13 @@ text\<open>
|
|||
the header consists of a sequence of commands used for introductory text elements not depending on
|
||||
any context. The context-definition contains an \<^boxed_isar>\<open>import\<close> and a
|
||||
\<^boxed_isar>\<open>keyword\<close> section, for example:
|
||||
\begin{isar}
|
||||
" theory Example (* Name of the 'theory' *)
|
||||
" imports (* Declaration of 'theory' dependencies *)
|
||||
" Main (* Imports a library called 'Main' *)
|
||||
" keywords (* Registration of keywords defined locally *)
|
||||
" requirement (* A command for describing requirements *)
|
||||
\end{isar}
|
||||
@{boxed_theory_text [display]\<open>
|
||||
theory Example (* Name of the 'theory' *)
|
||||
imports (* Declaration of 'theory' dependencies *)
|
||||
Main (* Imports a library called 'Main' *)
|
||||
keywords (* Registration of keywords defined locally *)
|
||||
requirement (* A command for describing requirements *)
|
||||
\<close>}
|
||||
where \<^boxed_isar>\<open>Example\<close> is the abstract name of the text-file, \<^boxed_isar>\<open>Main\<close> refers to an
|
||||
imported theory (recall that the import relation must be acyclic) and \inlineisar{keywords} are
|
||||
used to separate commands from each other.
|
||||
|
|
@ -124,9 +124,9 @@ text\<open>
|
|||
|
||||
@{boxed_theory_text [display] \<open>text\<open>This is a description.\<close>\<close> }
|
||||
|
||||
\begin{isar}
|
||||
text\<Open>This is a description.\<Close>
|
||||
\end{isar}
|
||||
@{boxed_theory_text [display]\<open>
|
||||
text\<open>This is a description.\<close>
|
||||
\<close>}
|
||||
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 *\<open>semantic macros\<close>, called antiquotations\<^bindex>\<open>antiquotation\<close>:
|
||||
|
|
@ -136,10 +136,10 @@ text\<open>
|
|||
for @{term "fac 5"} the result @{value "fac 5"}.\<close>\<close>
|
||||
}
|
||||
|
||||
\begin{isar}
|
||||
text\<Open>According to the *\<Open>reflexivity\<Close> axiom <@>{thm refl}, we obtain in \<Gamma>
|
||||
for <@>{term "fac 5"} the result <@>{value "fac 5"}.\<Close>
|
||||
\end{isar}
|
||||
@{boxed_theory_text [display]\<open>
|
||||
text\<open>According to the *\<open>reflexivity\<close> axiom <@>{thm refl}, we obtain in \<Gamma>
|
||||
for @{term "fac 5"} the result @{value "fac 5"}.\<close>
|
||||
\<close>}
|
||||
|
||||
|
||||
which is represented in the final document (\<^eg>, a PDF) by:
|
||||
|
|
|
|||
|
|
@ -465,10 +465,10 @@ text\<open>
|
|||
underlying ontology. We proceed by a definition of \inlineisar+introduction+'s, which we define
|
||||
as the extension of \inlineisar+text_section+ which is intended to capture common infrastructure:
|
||||
|
||||
\begin{isar}
|
||||
@{boxed_theory_text [display]\<open>
|
||||
doc_class introduction = text_section +
|
||||
comment :: string
|
||||
\end{isar}
|
||||
\<close>}
|
||||
|
||||
As a consequence of the definition as extension, the \inlineisar+introduction+ class
|
||||
inherits the attributes \inlineisar+main_author+ and \inlineisar+todo_list+ together with
|
||||
|
|
@ -476,7 +476,7 @@ doc_class introduction = text_section +
|
|||
|
||||
We proceed more or less conventionally by the subsequent sections:
|
||||
|
||||
\begin{isar}
|
||||
@{boxed_theory_text [display]\<open>
|
||||
doc_class technical = text_section +
|
||||
definition_list :: "string list" <= "[]"
|
||||
|
||||
|
|
@ -489,19 +489,19 @@ doc_class conclusion = text_section +
|
|||
doc_class related_work = conclusion +
|
||||
main_author :: "author option" <= None
|
||||
|
||||
\end{isar}
|
||||
\<close>}
|
||||
|
||||
Moreover, we model a document class for including figures (actually, this document class is already
|
||||
defined in the core ontology of \<^isadof>):
|
||||
|
||||
\begin{isar}
|
||||
@{boxed_theory_text [display]\<open>
|
||||
datatype placement = h | t | b | ht | hb
|
||||
doc_class figure = text_section +
|
||||
relative_width :: "int" (* percent of textwidth *)
|
||||
src :: "string"
|
||||
placement :: placement
|
||||
spawn_columns :: bool <= True
|
||||
\end{isar}
|
||||
\<close>}
|
||||
\<close>
|
||||
figure*[fig_figures::figure,spawn_columns=False,relative_width="85",src="''figures/Dogfood-figures''"]
|
||||
\<open> Ouroboros II: figures \ldots \<close>
|
||||
|
|
@ -513,14 +513,14 @@ text\<open>
|
|||
Finally, we define a monitor class definition that enforces a textual ordering
|
||||
in the document core by a regular expression:
|
||||
|
||||
\begin{isar}
|
||||
@{boxed_theory_text [display]\<open>
|
||||
doc_class article =
|
||||
style_id :: string <= "''LNCS''"
|
||||
version :: "(int \<times> int \<times> int)" <= "(0,0,0)"
|
||||
where "(title ~~ \<lbrakk>subtitle\<rbrakk> ~~ \<lbrace>author\<rbrace>$^+$+ ~~ abstract ~~
|
||||
introduction ~~ \<lbrace>technical || example\<rbrace>$^+$ ~~ conclusion ~~
|
||||
bibliography)"
|
||||
\end{isar}
|
||||
\<close>}
|
||||
\<close>
|
||||
|
||||
subsection*[scholar_pide::example]\<open>Editing Support for Academic Papers\<close>
|
||||
|
|
@ -607,7 +607,7 @@ text\<open>
|
|||
case-study~@{cite "bezzecchi.ea:making:2018"}. We start with an introduction of the concept of
|
||||
requirement:
|
||||
|
||||
\begin{isar}
|
||||
@{boxed_theory_text [display]\<open>
|
||||
doc_class requirement = long_name :: "string option"
|
||||
|
||||
doc_class requirement_analysis = no :: "nat"
|
||||
|
|
@ -620,7 +620,7 @@ datatype ass_kind = informal | semiformal | formal
|
|||
|
||||
doc_class assumption = requirement +
|
||||
assumption_kind :: ass_kind <= informal
|
||||
\end{isar}
|
||||
\<close>}
|
||||
|
||||
Such ontologies can be enriched by larger explanations and examples, which may help
|
||||
the team of engineers substantially when developing the central document for a certification,
|
||||
|
|
@ -644,23 +644,23 @@ is the category \<^emph>\<open>safety related application condition\<close> (or
|
|||
for short) which is used for \<^emph>\<open>ec\<close>'s that establish safety properties
|
||||
of the evaluation target. Their track-ability throughout the certification
|
||||
is therefore particularly critical. This is naturally modeled as follows:
|
||||
\begin{isar}
|
||||
@{boxed_theory_text [display]\<open>
|
||||
doc_class ec = assumption +
|
||||
assumption_kind :: ass_kind <= (*default *) formal
|
||||
|
||||
doc_class srac = ec +
|
||||
assumption_kind :: ass_kind <= (*default *) formal
|
||||
\end{isar}
|
||||
\<close>}
|
||||
|
||||
We now can, \<^eg>, write
|
||||
|
||||
\begin{isar}
|
||||
text*[ass123::SRAC]\<Open>
|
||||
@{boxed_theory_text [display]\<open>
|
||||
text*[ass123::SRAC]\<open>
|
||||
The overall sampling frequence of the odometer subsystem is therefore
|
||||
14 khz, which includes sampling, computing a$$nd result communication
|
||||
times \ldots
|
||||
\<Close>
|
||||
\end{isar}
|
||||
\<close>
|
||||
\<close>}
|
||||
|
||||
This will be shown in the PDF as follows:
|
||||
\<close>
|
||||
|
|
@ -739,7 +739,7 @@ text\<open>
|
|||
Furthermore, we assume a simple grade system (thus, some calculation is required). We
|
||||
can model this as follows:
|
||||
|
||||
\begin{isar}
|
||||
@{boxed_theory_text [display]\<open>
|
||||
doc_class Author = ...
|
||||
datatype Subject = algebra | geometry | statistical
|
||||
datatype Grade = A1 | A2 | A3
|
||||
|
|
@ -755,14 +755,14 @@ doc_class Exam_item = concerns :: "ContentClass set"
|
|||
doc_class Exam_item = concerns :: "ContentClass set"
|
||||
|
||||
type_synonym SubQuestion = string
|
||||
\end{isar}
|
||||
\<close>}
|
||||
|
||||
The heart of this ontology is an alternation of questions and answers, where the answers can
|
||||
consist of simple yes-no answers or lists of formulas. Since we do not assume familiarity of
|
||||
the students with Isabelle (\inlineisar+term+ would assume that this is a parse-able and
|
||||
type-checkable entity), we basically model a derivation as a sequence of strings:
|
||||
|
||||
\begin{isar}
|
||||
@{boxed_theory_text [display]\<open>
|
||||
doc_class Answer_Formal_Step = Exam_item +
|
||||
justification :: string
|
||||
"term" :: "string"
|
||||
|
|
@ -786,13 +786,13 @@ doc_class Exercise = Exam_item +
|
|||
content :: "(Task) list"
|
||||
concerns :: "ContentClass set" <= "UNIV"
|
||||
mark :: int
|
||||
\end{isar}
|
||||
\<close>}
|
||||
|
||||
In many institutions, having a rigorous process of validation for exam subjects makes sense: is
|
||||
the initial question correct? Is a proof in the sense of the question possible? We model the
|
||||
possibility that the @{term examiner} validates a question by a sample proof validated by Isabelle:
|
||||
|
||||
\begin{isar}
|
||||
@{boxed_theory_text [display]\<open>
|
||||
doc_class Validation =
|
||||
tests :: "term list" <="[]"
|
||||
proofs :: "thm list" <="[]"
|
||||
|
|
@ -806,7 +806,7 @@ doc_class MathExam=
|
|||
content :: "(Header + Author + Exercise) list"
|
||||
global_grade :: Grade
|
||||
where "\<lbrace>Author\<rbrace>$^+$ ~~ Header ~~ \<lbrace>Exercise ~~ Solution\<rbrace>$^+$ "
|
||||
\end{isar}
|
||||
\<close>}
|
||||
|
||||
In our scenario this sample proofs are completely \<^emph>\<open>intern\<close>, \ie, not exposed to the
|
||||
students but just additional material for the internal review process of the exam.
|
||||
|
|
@ -820,18 +820,18 @@ text\<open>
|
|||
using \<^LaTeX>{} as the underlying back-end. As Isabelle's document generation framework, it is
|
||||
possible to embed (nearly) arbitrary \<^LaTeX>-commands in text-commands, \<^eg>:
|
||||
|
||||
\begin{isar}
|
||||
text\<Open> This is \emph{emphasized} a$$nd this is a
|
||||
citation~\cite{brucker.ea:isabelle-ontologies:2018}\<Close>
|
||||
\end{isar}
|
||||
@{boxed_theory_text [display]\<open>
|
||||
text\<open> This is \emph{emphasized} a$$nd this is a
|
||||
citation~\cite{brucker.ea:isabelle-ontologies:2018}\<close>
|
||||
\<close>}
|
||||
|
||||
In general, we advise against this practice and, whenever positive, use the \<^isadof> (respetively
|
||||
Isabelle) provided alternatives:
|
||||
|
||||
\begin{isar}
|
||||
text\<Open> This is *\<Open>emphasized\<Close> a$$nd this is a
|
||||
citation <@>{cite "brucker.ea:isabelle-ontologies:2018"}.\<Close>
|
||||
\end{isar}
|
||||
@{boxed_theory_text [display]\<open>
|
||||
text\<open> This is *\<open>emphasized\<close> a$$nd this is a
|
||||
citation <@>{cite "brucker.ea:isabelle-ontologies:2018"}.\<close>
|
||||
\<close>}
|
||||
|
||||
Clearly, this is not always possible and, in fact, often \<^isadof> documents will contain
|
||||
\<^LaTeX>-commands, this should be restricted to layout improvements that otherwise are (currently)
|
||||
|
|
|
|||
|
|
@ -324,7 +324,7 @@ text\<open>
|
|||
The \<open>class_id\<close> is the full-qualified name of the document class and the list of \<open>attribute_decl\<close>
|
||||
needs to declare all attributes of the document class. Within the \LaTeX-definition of the document
|
||||
class representation, the identifier \inlineltx|#1| refers to the content of the main text of the
|
||||
document class (written in \inlineisar|\<Open> ... \<Close>|) and the attributes can be referenced
|
||||
document class (written in \inlineisar|\<open> ... \<close>|) and the attributes can be referenced
|
||||
by their name using the \inlineltx|\commandkey{...}|-command (see the documentation of the
|
||||
\LaTeX-package ``keycommand''~@{cite "chervet:keycommand:2010"} for details). Usually, the
|
||||
representations definition needs to be wrapped in a
|
||||
|
|
@ -363,7 +363,7 @@ shadow classes, with own attributes and, last not least, own definitions of inva
|
|||
from ours.
|
||||
|
||||
In particular, these shadow classes are used at present in \isadof:
|
||||
\begin{isar}
|
||||
@{boxed_theory_text [display]\<open>
|
||||
DOCUMENT_ALIKES =
|
||||
level :: "int option" <= "None"
|
||||
|
||||
|
|
@ -372,7 +372,7 @@ ASSERTION_ALIKES =
|
|||
|
||||
FORMAL_STATEMENT_ALIKE =
|
||||
properties :: "thm list"
|
||||
\end{isar}
|
||||
\<close>}
|
||||
|
||||
These shadow-classes correspond to semantic macros
|
||||
@{ML "Onto_Macros.enriched_document_command"},
|
||||
|
|
@ -390,12 +390,12 @@ text\<open>
|
|||
In particular it defines the super-class \inlineisar|text_element|: the
|
||||
root of all text-elements,
|
||||
|
||||
\begin{isar}
|
||||
@{boxed_theory_text [display]\<open>
|
||||
doc_class text_element =
|
||||
level :: "int option" <= "None"
|
||||
referentiable :: bool <= "False"
|
||||
variants :: "String.literal set" <= "{STR ''outline'', STR ''document''}"
|
||||
\end{isar}
|
||||
\<close>}
|
||||
|
||||
Here, \inlineisar|level| defines the section-level (\eg, using a \LaTeX-inspired hierarchy:
|
||||
from \inlineisar|Some -1| (corresponding to \inlineltx|\part|) to
|
||||
|
|
@ -407,13 +407,13 @@ doc_class text_element =
|
|||
|
||||
Similarly, we provide "minimal" instances of the \inlineisar+ASSERTION_ALIKES+
|
||||
and \inlineisar+FORMAL_STATEMENT_ALIKE+ shadow classes:
|
||||
\begin{isar}
|
||||
@{boxed_theory_text [display]\<open>
|
||||
doc_class assertions =
|
||||
properties :: "term list"
|
||||
|
||||
doc_class "thms" =
|
||||
properties :: "thm list"
|
||||
\end{isar}
|
||||
\<close>}
|
||||
\<close>
|
||||
|
||||
subsubsection\<open>Example: Text Elemens with Levels\<close>
|
||||
|
|
@ -421,7 +421,7 @@ text\<open>
|
|||
The category ``exported constraint (EC)'' is, in the file
|
||||
\path{ontologies/CENELEC_50128/CENELEC_50128.thy} defined as follows:
|
||||
|
||||
\begin{isar}
|
||||
@{boxed_theory_text [display]\<open>
|
||||
doc_class requirement = text_element +
|
||||
long_name :: "string option"
|
||||
is_concerned :: "role set"
|
||||
|
|
@ -429,7 +429,7 @@ doc_class AC = requirement +
|
|||
is_concerned :: "role set" <= "UNIV"
|
||||
doc_class EC = AC +
|
||||
assumption_kind :: ass_kind <= (*default *) formal
|
||||
\end{isar}
|
||||
\<close>}
|
||||
|
||||
We now define the document representations, in the file
|
||||
\path{ontologies/CENELEC_50128/DOF-CENELEC_50128.sty}. Let us assume that we want to
|
||||
|
|
@ -485,12 +485,12 @@ assert*[claim::assertions] "last[4::int] = 4"
|
|||
assert*[claim::assertions] "last[1,2,3,4::int] = 4"
|
||||
(*>*)
|
||||
text\<open>We want to check the consequences of this definition and can add the following statements:
|
||||
\begin{isar}
|
||||
text*[claim::assertions]\<Open>For non-empty lists, our definition yields indeed
|
||||
the last element of a list.\<Close>
|
||||
@{boxed_theory_text [display]\<open>
|
||||
text*[claim::assertions]\<open>For non-empty lists, our definition yields indeed
|
||||
the last element of a list.\<close>
|
||||
assert*[claim::assertions] "last[4::int] = 4"
|
||||
assert*[claim::assertions] "last[1,2,3,4::int] = 4"
|
||||
\end{isar}
|
||||
\<close>}
|
||||
\<close>
|
||||
|
||||
text\<open>As an \inlineisar+ASSERTION_ALIKES+, the \inlineisar+assertions+ class possesses a
|
||||
|
|
@ -502,19 +502,19 @@ text-element. Commands like \inlineisar+Definitions*+ or \inlineisar+Theorem*+ w
|
|||
subsection*["text-elements"::technical]\<open>Annotatable Top-level Text-Elements\<close>
|
||||
text\<open>
|
||||
While the default user interface for class definitions via the
|
||||
\inlineisar|text*\<Open> ... \<Close>|-command allow to access all features of the document
|
||||
\inlineisar|text*\<open> ... \<close>|-command allow to access all features of the document
|
||||
class, \isadof provides short-hands for certain, widely-used, concepts such as
|
||||
\inlineisar|title*\<Open> ... \<Close>| or \inlineisar|section*\<Open> ... \<Close>|, \eg:
|
||||
\inlineisar|title*\<open> ... \<close>| or \inlineisar|section*\<open> ... \<close>|, \eg:
|
||||
|
||||
\begin{isar}
|
||||
title*[title::title]\<Open>Isabelle/DOF\<Close>
|
||||
subtitle*[subtitle::subtitle]\<Open>User and Implementation Manual\<Close>
|
||||
text*[adb:: author, email="\<Open>a.brucker@exeter.ac.uk\<Close>",
|
||||
orcid="\<Open>0000-0002-6355-1200\<Close>", http_site="\<Open>https://brucker.ch/\<Close>",
|
||||
affiliation="\<Open>University of Exeter, Exeter, UK\<Close>"] \<Open>Achim D. Brucker\<Close>
|
||||
text*[bu::author, email = "\<Open>wolff@lri.fr\<Close>",
|
||||
affiliation = "\<Open>Université Paris-Saclay, LRI, Paris, France\<Close>"]\<Open>Burkhart Wolff\<Close>
|
||||
\end{isar}
|
||||
@{boxed_theory_text [display]\<open>
|
||||
title*[title::title]\<open>Isabelle/DOF\<close>
|
||||
subtitle*[subtitle::subtitle]\<open>User and Implementation Manual\<close>
|
||||
text*[adb:: author, email="\<open>a.brucker@exeter.ac.uk\<close>",
|
||||
orcid="\<open>0000-0002-6355-1200\<close>", http_site="\<open>https://brucker.ch/\<close>",
|
||||
affiliation="\<open>University of Exeter, Exeter, UK\<close>"] \<open>Achim D. Brucker\<close>
|
||||
text*[bu::author, email = "\<open>wolff@lri.fr\<close>",
|
||||
affiliation = "\<open>Université Paris-Saclay, LRI, Paris, France\<close>"]\<open>Burkhart Wolff\<close>
|
||||
\<close>}
|
||||
|
||||
In general, all standard text-elements from the Isabelle document model such
|
||||
as @{command "chapter"}, @{command "section"}, @{command "text"}, have in the \isadof
|
||||
|
|
@ -560,7 +560,7 @@ text\<open>
|
|||
First, new top-level keywords need to be declared in the \inlineisar|keywords|-section of
|
||||
the theory header defining new keywords:
|
||||
|
||||
\begin{isar}
|
||||
@{boxed_theory_text [display]\<open>
|
||||
theory
|
||||
...
|
||||
imports
|
||||
|
|
@ -570,7 +570,7 @@ theory
|
|||
begin
|
||||
...
|
||||
end
|
||||
\end{isar}
|
||||
\<close>}
|
||||
|
||||
Second, given an implementation of the functionality of the new keyword (implemented in SML),
|
||||
the new keyword needs to be registered, together with its parser, as outer syntax:
|
||||
|
|
@ -644,7 +644,7 @@ text\<open>
|
|||
example: \inlineisar+property = "[<@>{thm ''system_is_safe''}]"+ in a
|
||||
system context \inlineisar+\<theta>+ where this theorem is
|
||||
established. Similarly, attribute values like
|
||||
\inlineisar+property = "<@>{term \<Open>A \<leftrightarrow> B\<Close>}"+
|
||||
\inlineisar+property = "<@>{term \<open>A \<leftrightarrow> B\<close>}"+
|
||||
require that the HOL-string \inlineisar+A \<leftrightarrow> B+ is
|
||||
again type-checked and represents indeed a formula in $\theta$. Another instance of
|
||||
this process, which we call \<open>second-level type-checking\<close>, are term-constants
|
||||
|
|
@ -659,19 +659,20 @@ text\<open>
|
|||
accept-clause\index{accept-clause} contains a regular expression over class identifiers.
|
||||
For example:
|
||||
|
||||
\begin{isar}
|
||||
TODO bsub/esub
|
||||
@{boxed_theory_text [display]\<open>
|
||||
doc_class article = style_id :: string <= "''CENELEC_50128''"
|
||||
accepts "(title ~~ \<lbrace>author\<rbrace>\<bsup>+\<esup> ~~ abstract ~~ \<lbrace>introduction\<rbrace>\<bsup>+\<esup> ~~
|
||||
\<lbrace>technical || example\<rbrace>\<bsup>+\<esup> ~~ \<lbrace>conclusion\<rbrace>\<bsup>+\<esup>)"
|
||||
\end{isar}
|
||||
accepts "(title ~~ \<lbrace>author\<rbrace> bsup+esup ~~ abstract ~~ \<lbrace>introduction\<rbrace> bsup+esup ~~
|
||||
\<lbrace>technical || example\<rbrace> bsup+esup ~~ \<lbrace>conclusion\<rbrace> bsup+esup)"
|
||||
\<close>}
|
||||
|
||||
Semantically, monitors introduce a behavioral element into ODL:
|
||||
|
||||
\begin{isar}
|
||||
@{boxed_theory_text [display]\<open>
|
||||
open_monitor*[this::article] (* begin of scope of monitor "this" *)
|
||||
...
|
||||
close_monitor*[this] (* end of scope of monitor "this" *)
|
||||
\end{isar}
|
||||
\<close>}
|
||||
|
||||
Inside the scope of a monitor, all instances of classes mentioned in its accept-clause (the
|
||||
\<^emph>\<open>accept-set\<close>) have to appear in the order specified by the regular expression; instances not
|
||||
|
|
@ -714,12 +715,12 @@ text\<open>
|
|||
|
||||
In a high-level syntax, this type of constraints could be expressed, \eg, by:
|
||||
|
||||
\begin{isar}
|
||||
@{boxed_theory_text [display]\<open>
|
||||
(* 1 *) \<forall> x \<in> result. x@kind = pr$$oof \<leftrightarrow> x@kind \<noteq> []
|
||||
(* 2 *) \<forall> x \<in> conclusion. \<forall> y \<in> Domain(x@establish)
|
||||
\<rightarrow> \<exists> y \<in> Range(x@establish). (y,z) \<in> x@establish
|
||||
(* 3 *) \<forall> x \<in> introduction. finite(x@authored_by)
|
||||
\end{isar}
|
||||
\<close>}
|
||||
|
||||
where \inlineisar+result+, \inlineisar+conclusion+, and \inlineisar+introduction+ are the set of
|
||||
all possible instances of these document classes. All specified constraints are already checked
|
||||
|
|
|
|||
|
|
@ -139,9 +139,9 @@ val attributes =(Parse.$$$ "[" |-- (reference
|
|||
Altogether, this gives the extension of Isabelle/HOL with Isar syntax and semantics for the
|
||||
new \emph{command}:
|
||||
|
||||
\begin{isar}
|
||||
@{boxed_theory_text [display]\<open>
|
||||
declare_reference [lal::requirement, alpha="main", beta=42]
|
||||
\end{isar}
|
||||
\<close>}
|
||||
|
||||
The construction also generates implicitly some markup information; for example, when hovering
|
||||
over the \inlineisar|declare_reference| command in the IDE, a popup window with the text:
|
||||
|
|
@ -166,9 +166,9 @@ val _ = Theory.setup(
|
|||
syntax and the overall semantics. This code defines a generic antiquotation to be used in text
|
||||
elements such as
|
||||
|
||||
\begin{isar}
|
||||
text\<Open>as defined in <@>{docitem \<Open>d1\<Close>} ...\<Close>
|
||||
\end{isar}
|
||||
@{boxed_theory_text [display]\<open>
|
||||
text\<open>as defined in <@>{docitem \<open>d1\<close>} ...\<close>
|
||||
\<close>}
|
||||
|
||||
The subsequent registration \inlineisar+docitem_value+ binds code to a ML-antiquotation usable
|
||||
in an ML context for user-defined extensions; it permits the access to the current ``value''
|
||||
|
|
@ -176,8 +176,8 @@ text\<Open>as defined in <@>{docitem \<Open>d1\<Close>} ...\<Close>
|
|||
|
||||
It is possible to generate antiquotations \emph{dynamically}, as a consequence of a class
|
||||
definition in ODL. The processing of the ODL class \inlineisar+d$$efinition+ also \emph{generates}
|
||||
a text antiquotation \inlineisar+<@>{definition \<Open>d1\<Close>}+, which works similar to
|
||||
\inlineisar+<@>{docitem \<Open>d1\<Close>}+ except for an additional type-check that assures that
|
||||
a text antiquotation \inlineisar+<@>{definition \<open>d1\<close>}+, which works similar to
|
||||
\inlineisar+<@>{docitem \<open>d1\<close>}+ except for an additional type-check that assures that
|
||||
\inlineisar+d1+ is a reference to a definition. These type-checks support the subclass hierarchy.
|
||||
\<close>
|
||||
|
||||
|
|
|
|||
|
|
@ -119,6 +119,18 @@ France, and therefore granted with public funds of the Program ``Investissements
|
|||
\AtBeginDocument{\isabellestyle{literal}\newcommand{\lstnumberautorefname}{Line}}
|
||||
\renewcommand{\isacommand}[1]{\textcolor{OliveGreen!60}{\ttfamily\bfseries #1}}
|
||||
|
||||
\newenvironment{isarbox}
|
||||
{AAA - bu isarbox}
|
||||
{ZZZ - bu isarbox}
|
||||
\NewTColorBox[]{isarbox}{}{
|
||||
,boxrule=0pt
|
||||
,boxsep=0pt
|
||||
,colback=white!90!isar
|
||||
,enhanced jigsaw
|
||||
,borderline west={2pt}{0pt}{isar!60!black}
|
||||
,sharp corners
|
||||
% ,before skip=10pt
|
||||
% ,after skip=10pt
|
||||
,enlarge top by=0mm
|
||||
,enhanced
|
||||
,overlay={\node[draw,fill=isar!60!black,xshift=0pt,anchor=north
|
||||
east,font=\bfseries\footnotesize\color{white}]
|
||||
at (frame.north east) {Isar};}
|
||||
}
|
||||
|
|
|
|||
Loading…
Reference in New Issue