diff --git a/examples/scholarly_paper/2021-ITP-PMTI/ROOT b/examples/scholarly_paper/2021-ITP-PMTI/ROOT
index e577066b..3155be07 100644
--- a/examples/scholarly_paper/2021-ITP-PMTI/ROOT
+++ b/examples/scholarly_paper/2021-ITP-PMTI/ROOT
@@ -18,6 +18,8 @@ session "2021-ITP-PMTI" = "Isabelle_DOF" +
"figures/invariant-checking-violated-example.png"
"figures/inherited-invariant-checking-violated-example.png"
"figures/term-context-checking-example.png"
+ "figures/term-context-failed-checking-example.png"
"figures/term-context-evaluation-example.png"
+ "figures/term-context-failed-evaluation-example.png"
"figures/term-context-equality-evaluation-example.png"
"lstisadof.sty"
diff --git a/examples/scholarly_paper/2021-ITP-PMTI/document/figures/term-context-failed-checking-example.png b/examples/scholarly_paper/2021-ITP-PMTI/document/figures/term-context-failed-checking-example.png
new file mode 100644
index 00000000..76a25bc7
Binary files /dev/null and b/examples/scholarly_paper/2021-ITP-PMTI/document/figures/term-context-failed-checking-example.png differ
diff --git a/examples/scholarly_paper/2021-ITP-PMTI/document/figures/term-context-failed-evaluation-example.png b/examples/scholarly_paper/2021-ITP-PMTI/document/figures/term-context-failed-evaluation-example.png
new file mode 100644
index 00000000..3f59fbb3
Binary files /dev/null and b/examples/scholarly_paper/2021-ITP-PMTI/document/figures/term-context-failed-evaluation-example.png differ
diff --git a/examples/scholarly_paper/2021-ITP-PMTI/document/lstisadof-manual.sty b/examples/scholarly_paper/2021-ITP-PMTI/document/lstisadof-manual.sty
new file mode 100755
index 00000000..9c1589d1
--- /dev/null
+++ b/examples/scholarly_paper/2021-ITP-PMTI/document/lstisadof-manual.sty
@@ -0,0 +1,298 @@
+%% Copyright (C) 2018 The University of Sheffield
+%% 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
+%% of the LaTeX Project Public License Distributed from CTAN
+%% archives in directory macros/latex/base/lppl.txt; either
+%% version 1.3c of the License, or (at your option) any later version.
+%% OR
+%% The 2-clause BSD-style license.
+%%
+%% SPDX-License-Identifier: LPPL-1.3c+ OR BSD-2-Clause
+\usepackage{listings}
+\usepackage{listingsutf8}
+\usepackage{tikz}
+\usepackage[many]{tcolorbox}
+\tcbuselibrary{listings}
+\tcbuselibrary{skins}
+\usepackage{xstring}
+
+\definecolor{OliveGreen} {cmyk}{0.64,0,0.95,0.40}
+\definecolor{BrickRed} {cmyk}{0,0.89,0.94,0.28}
+\definecolor{Blue} {cmyk}{1,1,0,0}
+\definecolor{CornflowerBlue}{cmyk}{0.65,0.13,0,0}
+
+
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%
+%% Hack: re-defining tag types for supporting highlighting of antiquotations
+\gdef\lst@tagtypes{s}
+\gdef\lst@TagKey#1#2{%
+ \lst@Delim\lst@tagstyle #2\relax
+ {Tag}\lst@tagtypes #1%
+ {\lst@BeginTag\lst@EndTag}%
+ \@@end\@empty{}}
+\lst@Key{tag}\relax{\lst@TagKey\@empty{#1}}
+\lst@Key{tagstyle}{}{\def\lst@tagstyle{#1}}
+\lst@AddToHook{EmptyStyle}{\let\lst@tagstyle\@empty}
+\gdef\lst@BeginTag{%
+ \lst@DelimOpen
+ \lst@ifextags\else
+ {\let\lst@ifkeywords\iftrue
+ \lst@ifmarkfirstintag \lst@firstintagtrue \fi}}
+\lst@AddToHookExe{ExcludeDelims}{\let\lst@ifextags\iffalse}
+\gdef\lst@EndTag{\lst@DelimClose\lst@ifextags\else}
+\lst@Key{usekeywordsintag}t[t]{\lstKV@SetIf{#1}\lst@ifusekeysintag}
+\lst@Key{markfirstintag}f[t]{\lstKV@SetIf{#1}\lst@ifmarkfirstintag}
+\gdef\lst@firstintagtrue{\global\let\lst@iffirstintag\iftrue}
+\global\let\lst@iffirstintag\iffalse
+ \lst@AddToHook{PostOutput}{\lst@tagresetfirst}
+ \lst@AddToHook{Output}
+ {\gdef\lst@tagresetfirst{\global\let\lst@iffirstintag\iffalse}}
+ \lst@AddToHook{OutputOther}{\gdef\lst@tagresetfirst{}}
+\lst@AddToHook{Output}
+ {\ifnum\lst@mode=\lst@tagmode
+ \lst@iffirstintag \let\lst@thestyle\lst@gkeywords@sty \fi
+ \lst@ifusekeysintag\else \let\lst@thestyle\lst@gkeywords@sty\fi
+ \fi}
+\lst@NewMode\lst@tagmode
+\gdef\lst@Tag@s#1#2\@empty#3#4#5{%
+ \lst@CArg #1\relax\lst@DefDelimB {}{}%
+ {\ifnum\lst@mode=\lst@tagmode \expandafter\@gobblethree \fi}%
+ #3\lst@tagmode{#5}%
+ \lst@CArg #2\relax\lst@DefDelimE {}{}{}#4\lst@tagmode}%
+\gdef\lst@BeginCDATA#1\@empty{%
+ \lst@TrackNewLines \lst@PrintToken
+ \lst@EnterMode\lst@GPmode{}\let\lst@ifmode\iffalse
+ \lst@mode\lst@tagmode #1\lst@mode\lst@GPmode\relax\lst@modetrue}
+%
+\def\beginlstdelim#1#2#3%
+{%
+ \def\endlstdelim{\texttt{\textbf{\color{black!60}#2}}\egroup}%
+ \ttfamily\textbf{\color{black!60}#1}\bgroup\rmfamily\color{#3}\aftergroup\endlstdelim%
+}
+%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%
+\providecolor{isar}{named}{blue}
+\renewcommand{\isacommand}[1]{\textcolor{OliveGreen!60}{\ttfamily\bfseries #1}}
+\newcommand{\inlineisarbox}[1]{#1}
+\NewTColorBox[]{isarbox}{}{
+ ,boxrule=0pt
+ ,boxsep=0pt
+ ,colback=white!90!isar
+ ,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
+ ,enhanced
+ ,overlay={\node[draw,fill=isar!60!black,xshift=0pt,anchor=north
+ east,font=\bfseries\footnotesize\color{white}]
+ at (frame.north east) {Isar};}
+}
+%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%
+\providecolor{out}{named}{green}
+\newtcblisting{out}[1][]{%
+ listing only%
+ ,boxrule=0pt
+ ,boxsep=0pt
+ ,colback=white!90!out
+ ,enhanced jigsaw
+ ,borderline west={2pt}{0pt}{out!60!black}
+ ,sharp corners
+ % ,before skip=10pt
+ % ,after skip=10pt
+ ,enlarge top by=0mm
+ ,enhanced
+ ,overlay={\node[draw,fill=out!60!black,xshift=0pt,anchor=north
+ east,font=\bfseries\footnotesize\color{white}]
+ at (frame.north east) {Document};}
+ ,listing options={
+ breakatwhitespace=true
+ ,columns=flexible%
+ ,basicstyle=\small\rmfamily
+ ,mathescape
+ ,#1
+ }
+ }%
+%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%
+\lstloadlanguages{ML}
+\providecolor{sml}{named}{red}
+\lstdefinestyle{sml}{
+ basicstyle=\ttfamily,%
+ commentstyle=\itshape,%
+ keywordstyle=\bfseries\color{CornflowerBlue},%
+ ndkeywordstyle=\color{green},%
+ language=ML
+% ,literate={%
+% {<@>}{@}1%
+% }
+ ,keywordstyle=[6]{\itshape}%
+ ,morekeywords=[6]{args_type}%
+ ,tag=**[s]{@\{}{\}}%
+ ,tagstyle=\color{CornflowerBlue}%
+ ,markfirstintag=true%
+}%
+\def\inlinesml{\lstinline[style=sml,breaklines=true,mathescape,breakatwhitespace=true]}
+\newtcblisting{sml}[1][]{%
+ listing only%
+ ,boxrule=0pt
+ ,boxsep=0pt
+ ,colback=white!90!sml
+ ,enhanced jigsaw
+ ,borderline west={2pt}{0pt}{sml!60!black}
+ ,sharp corners
+ % ,before skip=10pt
+ % ,after skip=10pt
+ ,enlarge top by=0mm
+ ,enhanced
+ ,overlay={\node[draw,fill=sml!60!black,xshift=0pt,anchor=north
+ east,font=\bfseries\footnotesize\color{white}]
+ at (frame.north east) {SML};}
+ ,listing options={
+ style=sml
+ ,columns=flexible%
+ ,basicstyle=\small\ttfamily
+ ,mathescape
+ ,#1
+ }
+ }%
+%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%
+\lstloadlanguages{TeX}
+\providecolor{ltx}{named}{yellow}
+\lstdefinestyle{lltx}{language=[AlLaTeX]TeX,
+ ,basicstyle=\ttfamily%
+ ,showspaces=false%
+ ,escapechar=ë
+ ,showlines=false%
+ ,morekeywords={newisadof}
+ % ,keywordstyle=\bfseries%
+ % Defining 2-keywords
+ ,keywordstyle=[1]{\color{BrickRed!60}\bfseries}%
+ % Defining 3-keywords
+ ,keywordstyle=[2]{\color{OliveGreen!60}\bfseries}%
+ % Defining 4-keywords
+ ,keywordstyle=[3]{\color{black!60}\bfseries}%
+ % Defining 5-keywords
+ ,keywordstyle=[4]{\color{Blue!70}\bfseries}%
+ % Defining 6-keywords
+ ,keywordstyle=[5]{\itshape}%
+ %
+}
+\lstdefinestyle{ltx}{style=lltx,
+ basicstyle=\ttfamily\small}%
+\def\inlineltx{\lstinline[style=ltx, breaklines=true,columns=fullflexible]}
+% see
+% https://tex.stackexchange.com/questions/247643/problem-with-tcblisting-first-listed-latex-command-is-missing
+\NewTCBListing{ltx}{ !O{} }{%
+ listing only%
+ ,boxrule=0pt
+ ,boxsep=0pt
+ ,colback=white!90!ltx
+ ,enhanced jigsaw
+ ,borderline west={2pt}{0pt}{ltx!60!black}
+ ,sharp corners
+ % ,before skip=10pt
+ % ,after skip=10pt
+ ,enlarge top by=0mm
+ ,enhanced
+ ,overlay={\node[draw,fill=ltx!60!black,xshift=0pt,anchor=north
+ east,font=\bfseries\footnotesize\color{white}]
+ at (frame.north east) {\LaTeX};}
+ ,listing options={
+ style=lltx,
+ ,columns=flexible%
+ ,basicstyle=\small\ttfamily
+ ,#1
+ }
+ }%
+%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%
+\providecolor{bash}{named}{black}
+\lstloadlanguages{bash}
+\lstdefinestyle{bash}{%
+ language=bash
+ ,escapechar=ë
+ ,basicstyle=\ttfamily%
+ ,showspaces=false%
+ ,showlines=false%
+ ,columns=flexible%
+ % ,keywordstyle=\bfseries%
+ % Defining 2-keywords
+ ,keywordstyle=[1]{\color{BrickRed!60}\bfseries}%
+ % Defining 3-keywords
+ ,keywordstyle=[2]{\color{OliveGreen!60}\bfseries}%
+ % Defining 4-keywords
+ ,keywordstyle=[3]{\color{black!60}\bfseries}%
+ % Defining 5-keywords
+ ,keywordstyle=[4]{\color{Blue!80}\bfseries}%
+ ,alsoletter={*,-,:,~,/}
+ ,morekeywords=[4]{}%
+ % Defining 6-keywords
+ ,keywordstyle=[5]{\itshape}%
+ %
+}
+\def\inlinebash{\lstinline[style=bash, breaklines=true,columns=fullflexible]}
+\newcommand\@isabsolutepath[3]{%
+ \StrLeft{#1}{1}[\firstchar]%
+ \IfStrEq{\firstchar}{/}{#2}{#3}%
+}
+
+\newcommand{\@homeprefix}[1]{%
+ \ifthenelse{\equal{#1}{}}{\textasciitilde}{\textasciitilde/}%
+}
+
+\newcommand{\prompt}[1]{%
+ \color{Blue!80}\textbf{\texttt{%
+ achim@logicalhacking:{\@isabsolutepath{#1}{#1}{\@homeprefix{#1}#1}}\$}}%
+}
+\newtcblisting{bash}[1][]{%
+ listing only%
+ ,boxrule=0pt
+ ,boxsep=0pt
+ ,colback=white!90!bash
+ ,enhanced jigsaw
+ ,borderline west={2pt}{0pt}{bash!60!black}
+ ,sharp corners
+ % ,before skip=10pt
+ % ,after skip=10pt
+ ,enlarge top by=0mm
+ ,enhanced
+ ,overlay={\node[draw,fill=bash!60!black,xshift=0pt,anchor=north
+ east,font=\bfseries\footnotesize\color{white}]
+ at (frame.north east) {Bash};}
+ ,listing options={
+ style=bash
+ ,columns=flexible%
+ ,breaklines=true%
+ ,prebreak=\mbox{\space\textbackslash}%
+ ,basicstyle=\small\ttfamily%
+ ,#1
+ }
+ }%
+%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
diff --git a/examples/scholarly_paper/2021-ITP-PMTI/paper.thy b/examples/scholarly_paper/2021-ITP-PMTI/paper.thy
index e0b1e66e..b6b10f56 100644
--- a/examples/scholarly_paper/2021-ITP-PMTI/paper.thy
+++ b/examples/scholarly_paper/2021-ITP-PMTI/paper.thy
@@ -431,13 +431,14 @@ text\
and can now be specified in common HOL syntax.
One can now specify the constraints using the keyword \<^theory_text>\invariant\ in the class definition.
If we take back the ontology example for mathematical papers
- of~@{cite "brucker.ea:isabelledof:2019"} (ADD LISTING REFERENCE!!!),
+ of~@{cite "brucker.ea:isabelledof:2019"} (see ADD LISTING REFERENCE!!!),
it was proposed to specify some constraints like that any instance of a \<^emph>\result\ class
finally has a non-empty property list, if its \<^theory_text>\kind\ is \<^theory_text>\"proof"\
(see the \<^theory_text>\invariant has_property\), or that
the \<^theory_text>\establish\ relation between \<^theory_text>\claim\ and \<^theory_text>\result\ must be defined when an instance
- of the class \<^theory_text>\conclusion\ is defined (see the \<^theory_text>\invariant establish_defined\).
-@{boxed_theory_text [display,indent=10, margin=70] \
+ of the class \<^theory_text>\conclusion\ is defined (see the \<^theory_text>\invariant establish_defined\).
+\begin{figure}
+@{boxed_theory_text [display] \
doc_class author =
email :: "string" <= "''''"
doc_class text_section =
@@ -464,7 +465,9 @@ doc_class conclusion = text_section +
invariant establisg_defined :: "\ x. x \ Domain (establish \)
\ (\ y \ Range (establish \). (x, y) \ establish \)"
\}
-
+\caption{Excerpt of an ontology example for mathematical papers.}
+\label{fig-ontology-example}
+\end{figure}
In our example, the invariant \<^theory_text>\author_finite \ of the class \<^theory_text>\introduction\ enforces
that the user sets the \<^theory_text>\authored_by\ set.
@@ -477,15 +480,21 @@ doc_class conclusion = text_section +
of the future instance of the class \<^theory_text>\conclusion\.
Now we can define some instances:
+\begin{figure}
@{boxed_theory_text [display] \
text*[church::author, email="\church@lambda.org\"]\\
text*[resultProof::result, evidence = "proof", property="[@{thm \HOL.refl\}]"]\\
+text*[resultProof2::result, evidence = "proof", property="[@{thm \HOL.sym\}]"]\\
+
text*[introduction1::introduction, authored_by = "{@{author \church\}}", level = "Some 0"]\\
text*[claimNotion::claim, authored_by = "{@{author \church\}}", based_on= "[\Notion1\, \Notion2\]", level = "Some 0"]\\
\}
+\caption{Some instances of the classes of the ontology in the \autoref{fig-ontology-example}.}
+\label{fig-instances-example}
+\end{figure}
\
(*<*)
@@ -507,7 +516,7 @@ text\
constraint specified in the \<^theory_text>\force_level\ invariant,
when we specify the \<^theory_text>\level\ attribute of \<^theory_text>\introduction\ to \<^theory_text>\Some 0\.
The \<^theory_text>\force_level\ invariant forces the value of the argument
- of the attribute \<^theory_text>\level\ option type to be greater than 1.
+ of the attribute \<^theory_text>\level\ to be greater than 1.
\
figure*[
@@ -522,7 +531,7 @@ declare_reference*["inherited-invariant-checking-figure"::figure]
(*>*)
text\
- Classes inherit the invariants from their superclasses.
+ Classes inherit the invariants from their superclass.
As the class \<^theory_text>\claim\ is a subsclass
of the class \<^theory_text>\introduction\, it inherits the \<^theory_text>\introduction\ invariants.
Hence the \<^theory_text>\force_level\ invariant is checked
@@ -538,35 +547,6 @@ figure*[
from the class \<^theory_text>\introduction\ and is violated by the instance \<^theory_text>\claimNotion\.
\
-(*
-text\For example, with the following two classes:
-\<^theory_text>\
-doc_class class_inv1 =
- int1 :: "int"
- invariant inv1 :: "int1 \ \ 3"
-
-doc_class class_inv2 = class_inv1 +
- int2 :: "int"
- invariant inv2 :: "int2 \ < 2"
-\
-
- as the class \<^theory_text>\class_inv2\ is a subsclass
- of the class \<^theory_text>\class_inv1\, it inherits \<^theory_text>\class_inv1\ invariants.
- Hence the \<^theory_text>\inv1\ invariant is checked
- when the instance \<^theory_text>\testinv2\ is defined, like we can see in .
-
- Now let's define two instances, one of each class:\
-
-
-
-text\
-\<^theory_text>\
-text*[testinv1::class_inv1, int1=4]\lorem ipsum...\
-text*[testinv2::class_inv2, int1=3, int2=1]\lorem ipsum...\
-\
-\
-*)
-
text\
The value of each attribute defined for the instances is checked against their classes invariants.
As the class \<^theory_text>\class_inv2\ is a subsclass of the class \<^theory_text>\class_inv1\,
@@ -574,37 +554,97 @@ text\
Hence the \<^theory_text>\int1\ invariant is checked when the instance \<^theory_text>\testinv2\ is defined.\
text\
- Isabelle/HOl provides commands which type-check and print terms (the command \<^theory_text>\term\)
- and evaluates and print a term (the command \<^theory_text>\value\).
- We provide the equivalent commands, respectively \<^theory_text>\term*\ and \<^theory_text>\value*\.
- These commands add up type-checking and expanding of isabelle/DOF antiquotations
- in a own validation phase.
+ To offer a smooth integration into the theory development process,
+ Isabelle/HOL should be able to dynamically interpret the source document.
+ But the specific antiquotations introduced by Isabelle/DOF are not directly recognized
+ by Isabelle/HOL, and the process of term checking and evaluation must be enriched.
+ Previous works added a validation step fo the SML and semi-formal text contexts.
+ But to support Isabelle/DOF antiquotations in the term contexts, the validation step must
+ be enriched and a new step, which we call \<^emph>\elaboration\ must be added to allow
+ these antiquotations in \\\-terms.
+ The resulting process encompasses the following steps:
+ \<^item> Parse the term which represents the object;
+ \<^item> Infer the type of the term;
+ \<^item> Certify the term;
+ \<^item> Pass on the information to PIDE;
+ \<^item> Validate the term: the Isabelle/DOF antiquotations terms are parsed and type-checked;
+ Validate the term: a step to understand the reference
+ which refers to the object.
+
+ This step is mandatory because the ontology framework adds
+ up objects not directly recognized by Isabelle/HOL;
+
+ \<^item> Elaborate: the Isabelle/DOF antiquotations terms are expanded.
+ The antiquotations are replaced by the objects in HOL they reference
+ i.e. a \(\lambda\)-calculus term;
+ \<^item> Code generation:
+ \<^item> Evaluation of HOL expressions with ontological annotations,
+ \<^item> Implementation of the ontological invariants processed simultaneously
+ with the generation of the document (a theory in HOL).
+
+ Isabelle/HOL provides commands to type-check and print terms (the command \<^theory_text>\term\)
+ and evaluate and print a term (the command \<^theory_text>\value\).
+ We provide the equivalent commands, respectively \<^theory_text>\term*\ and \<^theory_text>\value*\, which support
+ the validation and elaboration phase.
+ This allow a smooth integration into the \<^emph>\formal\ theory development process.
+\
+
+(*<*)
+declare_reference*["type-checking-example"::side_by_side_figure]
+(*>*)
+
+text\
For example one can now reference a class instance in a \<^theory_text>\term*\ command:
@{theory_text [display,indent=10, margin=70] \
term*\@{author \church\}\
\}
The term \<^theory_text>\@{author \church\}\ is type-checked, \<^ie>, the command \<^theory_text>\term*\ checks that
-\<^theory_text>\church\ references a term of type \<^theory_text>\author\.
-
- and the and we would like
-Isabelle to check that this instance is indeed an instance of this class.
-Here, we want to reference the instance \<^theory_text>\@{docitem \xcv4\}\ previously defined.
-We can use the term* command which extends the classic term command
-and does the appropriate checking.
-@{theory_text [display,indent=10, margin=70] \
-term*\@{F \xcv4\}\
-\}
-We can also reference an attribute of the instance.
-Here we reference the attribute r of the class F which has the type @{typ \thm list\}.
-
-@{theory_text [display,indent=10, margin=70] \
-term*\r @{F \xcv4\}\
-
-term \@{A \xcv2\}\
-\}
+\<^theory_text>\church\ references a term of type \<^theory_text>\author\
+(see \<^side_by_side_figure>\type-checking-example\).
\
+side_by_side_figure*[
+ "type-checking-example"::side_by_side_figure
+ , anchor="''fig-term-type-checking-ex''"
+ , caption="''church is an existing instance.''"
+ , relative_width="48"
+ , src="''figures/term-context-checking-example''"
+ , anchor2="''fig-term-type-checking-failed-ex''"
+ , caption2="''The churche instance is not defined.''"
+ , relative_width2="48"
+ , src2="''figures/term-context-failed-checking-example''"
+]\Type-checking of antiquotations in term context.\
+
+(*<*)
+declare_reference*["evaluation-example"::side_by_side_figure]
+(*>*)
+
+text\
+ This \<^theory_text>\value*\ command:
+@{theory_text [display,indent=10, margin=70] \
+value*\email @{author \church\}\
+\}
+
+type-checks the antiquotation \<^theory_text>\@{author \church\}\,
+and then returns the value of the \<^theory_text>\email\ attribute for the \<^theory_text>\church\ instance,
+\<^ie> the HOL string \<^term>\''church@lambda.org''\
+(see \<^side_by_side_figure>\evaluation-example\).
+\
+
+side_by_side_figure*[
+ "evaluation-example"::side_by_side_figure
+ , anchor="''fig-term-evaluation-ex''"
+ , caption="''A Text-Element as Requirement.''"
+ , relative_width="48"
+ , src="''figures/term-context-evaluation-example''"
+ , anchor2="''fig-term-failed-evaluation-ex''"
+ , caption2="''Referencing a Requirement.''"
+ , relative_width2="48"
+ , src2="''figures/term-context-failed-evaluation-example''"
+]\Evaluation of antiquotations in term context.\
+
+(*
figure*[
"term-context-checking-example-figure"::figure
, relative_width="99"
@@ -620,27 +660,27 @@ figure*[
]\The invariant \<^theory_text>\force_level\ of the class claim is inherited
from the class \<^theory_text>\introduction\ and is violated by the instance \<^theory_text>\claimNotion\.
\
+*)
-figure*[
- "term-context-equality-evaluation-figure"::figure
- , relative_width="99"
- , src="''figures/term-context-equality-evaluation-example''"
-]\The invariant \<^theory_text>\force_level\ of the class claim is inherited
- from the class \<^theory_text>\introduction\ and is violated by the instance \<^theory_text>\claimNotion\.
+(*<*)
+declare_reference*["term-context-equality-evaluation"::figure]
+(*>*)
+
+text\
+We can even compare classes. \<^figure>\term-context-equality-evaluation\