--- a/doc-src/Classes/Thy/Classes.thy Tue Mar 03 11:00:51 2009 +0100
+++ b/doc-src/Classes/Thy/Classes.thy Tue Mar 03 13:20:53 2009 +0100
@@ -2,8 +2,6 @@
imports Main Setup
begin
-chapter {* Haskell-style classes with Isabelle/Isar *}
-
section {* Introduction *}
text {*
@@ -17,10 +15,11 @@
types for @{text "\<alpha>"}, which is achieved by splitting introduction
of the @{text eq} function from its overloaded definitions by means
of @{text class} and @{text instance} declarations:
+ \footnote{syntax here is a kind of isabellized Haskell}
\begin{quote}
- \noindent@{text "class eq where"}\footnote{syntax here is a kind of isabellized Haskell} \\
+ \noindent@{text "class eq where"} \\
\hspace*{2ex}@{text "eq \<Colon> \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool"}
\medskip\noindent@{text "instance nat \<Colon> eq where"} \\
@@ -355,8 +354,8 @@
text {*
\noindent essentially introduces the locale
-*} setup %invisible {* Sign.add_path "foo" *}
-
+*} (*<*)setup %invisible {* Sign.add_path "foo" *}
+(*>*)
locale %quote idem =
fixes f :: "\<alpha> \<Rightarrow> \<alpha>"
assumes idem: "f (f x) = f x"
@@ -368,10 +367,10 @@
text {*
\noindent The connection to the type system is done by means
of a primitive axclass
-*} setup %invisible {* Sign.add_path "foo" *}
-
+*} (*<*)setup %invisible {* Sign.add_path "foo" *}
+(*>*)
axclass %quote idem < type
- idem: "f (f x) = f x" setup %invisible {* Sign.parent_path *}
+ idem: "f (f x) = f x" (*<*)setup %invisible {* Sign.parent_path *}(*>*)
text {* \noindent together with a corresponding interpretation: *}
@@ -383,8 +382,8 @@
\noindent This gives you at hand the full power of the Isabelle module system;
conclusions in locale @{text idem} are implicitly propagated
to class @{text idem}.
-*} setup %invisible {* Sign.parent_path *}
-
+*} (*<*)setup %invisible {* Sign.parent_path *}
+(*>*)
subsection {* Abstract reasoning *}
text {*
@@ -505,7 +504,7 @@
qed
text {*
- \noindent The logical proof is carried out on the locale level.
+ The logical proof is carried out on the locale level.
Afterwards it is propagated
to the type system, making @{text group} an instance of
@{text monoid} by adding an additional edge
@@ -541,7 +540,7 @@
\label{fig:subclass}
\end{center}
\end{figure}
-7
+
For illustration, a derived definition
in @{text group} which uses @{text pow_nat}:
*}
--- a/doc-src/Classes/Thy/Setup.thy Tue Mar 03 11:00:51 2009 +0100
+++ b/doc-src/Classes/Thy/Setup.thy Tue Mar 03 13:20:53 2009 +0100
@@ -1,8 +1,8 @@
theory Setup
imports Main Code_Integer
uses
- "../../../antiquote_setup"
- "../../../more_antiquote"
+ "../../antiquote_setup"
+ "../../more_antiquote"
begin
ML {* Code_Target.code_width := 74 *}
--- a/doc-src/Classes/Thy/document/Classes.tex Tue Mar 03 11:00:51 2009 +0100
+++ b/doc-src/Classes/Thy/document/Classes.tex Tue Mar 03 13:20:53 2009 +0100
@@ -18,10 +18,6 @@
%
\endisadelimtheory
%
-\isamarkupchapter{Haskell-style classes with Isabelle/Isar%
-}
-\isamarkuptrue%
-%
\isamarkupsection{Introduction%
}
\isamarkuptrue%
@@ -37,10 +33,11 @@
types for \isa{{\isasymalpha}}, which is achieved by splitting introduction
of the \isa{eq} function from its overloaded definitions by means
of \isa{class} and \isa{instance} declarations:
+ \footnote{syntax here is a kind of isabellized Haskell}
\begin{quote}
- \noindent\isa{class\ eq\ where}\footnote{syntax here is a kind of isabellized Haskell} \\
+ \noindent\isa{class\ eq\ where} \\
\hspace*{2ex}\isa{eq\ {\isasymColon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ bool}
\medskip\noindent\isa{instance\ nat\ {\isasymColon}\ eq\ where} \\
@@ -597,24 +594,21 @@
\noindent essentially introduces the locale%
\end{isamarkuptext}%
\isamarkuptrue%
-%
+\ %
\isadeliminvisible
-\ %
+%
\endisadeliminvisible
%
\isataginvisible
-\isacommand{setup}\isamarkupfalse%
-\ {\isacharverbatimopen}\ Sign{\isachardot}add{\isacharunderscore}path\ {\isachardoublequote}foo{\isachardoublequote}\ {\isacharverbatimclose}%
+%
\endisataginvisible
{\isafoldinvisible}%
%
\isadeliminvisible
%
\endisadeliminvisible
-\isanewline
%
\isadelimquote
-\isanewline
%
\endisadelimquote
%
@@ -654,31 +648,28 @@
of a primitive axclass%
\end{isamarkuptext}%
\isamarkuptrue%
-%
+\ %
\isadeliminvisible
-\ %
+%
\endisadeliminvisible
%
\isataginvisible
-\isacommand{setup}\isamarkupfalse%
-\ {\isacharverbatimopen}\ Sign{\isachardot}add{\isacharunderscore}path\ {\isachardoublequote}foo{\isachardoublequote}\ {\isacharverbatimclose}%
+%
\endisataginvisible
{\isafoldinvisible}%
%
\isadeliminvisible
%
\endisadeliminvisible
-\isanewline
%
\isadelimquote
-\isanewline
%
\endisadelimquote
%
\isatagquote
\isacommand{axclass}\isamarkupfalse%
\ idem\ {\isacharless}\ type\isanewline
-\ \ idem{\isacharcolon}\ {\isachardoublequoteopen}f\ {\isacharparenleft}f\ x{\isacharparenright}\ {\isacharequal}\ f\ x{\isachardoublequoteclose}%
+\ \ idem{\isacharcolon}\ {\isachardoublequoteopen}f\ {\isacharparenleft}f\ x{\isacharparenright}\ {\isacharequal}\ f\ x{\isachardoublequoteclose}\ %
\endisatagquote
{\isafoldquote}%
%
@@ -687,12 +678,11 @@
\endisadelimquote
%
\isadeliminvisible
-\ %
+%
\endisadeliminvisible
%
\isataginvisible
-\isacommand{setup}\isamarkupfalse%
-\ {\isacharverbatimopen}\ Sign{\isachardot}parent{\isacharunderscore}path\ {\isacharverbatimclose}%
+%
\endisataginvisible
{\isafoldinvisible}%
%
@@ -729,14 +719,13 @@
to class \isa{idem}.%
\end{isamarkuptext}%
\isamarkuptrue%
-%
+\ %
\isadeliminvisible
-\ %
+%
\endisadeliminvisible
%
\isataginvisible
-\isacommand{setup}\isamarkupfalse%
-\ {\isacharverbatimopen}\ Sign{\isachardot}parent{\isacharunderscore}path\ {\isacharverbatimclose}%
+%
\endisataginvisible
{\isafoldinvisible}%
%
@@ -978,7 +967,7 @@
\endisadelimquote
%
\begin{isamarkuptext}%
-\noindent The logical proof is carried out on the locale level.
+The logical proof is carried out on the locale level.
Afterwards it is propagated
to the type system, making \isa{group} an instance of
\isa{monoid} by adding an additional edge
@@ -1010,11 +999,11 @@
\end{picture}
\caption{Subclass relationship of monoids and groups:
before and after establishing the relationship
- \isa{group\ {\isasymsubseteq}\ monoid}; transitive edges left out.}
+ \isa{group\ {\isasymsubseteq}\ monoid}; transitive edges are left out.}
\label{fig:subclass}
\end{center}
\end{figure}
-7
+
For illustration, a derived definition
in \isa{group} which uses \isa{pow{\isacharunderscore}nat}:%
\end{isamarkuptext}%
--- a/doc-src/Classes/classes.tex Tue Mar 03 11:00:51 2009 +0100
+++ b/doc-src/Classes/classes.tex Tue Mar 03 13:20:53 2009 +0100
@@ -1,5 +1,5 @@
-\documentclass[12pt,a4paper,fleqn]{report}
+\documentclass[12pt,a4paper,fleqn]{article}
\usepackage{latexsym,graphicx}
\usepackage[refpage]{nomencl}
\usepackage{../iman,../extra,../isar,../proof}
@@ -21,7 +21,7 @@
\maketitle
\begin{abstract}
- This tutorial introduces the look-and-feel of Isar type classes
+ \noindent This tutorial introduces the look-and-feel of Isar type classes
to the end-user; Isar type classes are a convenient mechanism
for organizing specifications, overcoming some drawbacks
of raw axiomatic type classes. Essentially, they combine
--- a/doc-src/Classes/style.sty Tue Mar 03 11:00:51 2009 +0100
+++ b/doc-src/Classes/style.sty Tue Mar 03 13:20:53 2009 +0100
@@ -3,6 +3,9 @@
\newcommand{\tocentry}[1]{\cleardoublepage\phantomsection\addcontentsline{toc}{chapter}{#1}
\@mkboth{\MakeUppercase{#1}}{\MakeUppercase{#1}}}
+%% paragraphs
+\setlength{\parindent}{1em}
+
%% references
\newcommand{\secref}[1]{\S\ref{#1}}
\newcommand{\figref}[1]{figure~\ref{#1}}
@@ -17,23 +20,25 @@
%% verbatim text
\newcommand{\isatypewriter}{\fontsize{9pt}{0pt}\tt\renewcommand{\baselinestretch}{1}\setlength{\baselineskip}{9pt}}
-%% quoted segments
-\makeatletter
+%% quote environment
\isakeeptag{quote}
-\newenvironment{quotesegment}{\begin{quote}\isa@parindent\parindent\parindent0pt\isa@parskip\parskip\parskip0pt}{\end{quote}}
-\renewcommand{\isatagquote}{\begin{quotesegment}}
-\renewcommand{\endisatagquote}{\end{quotesegment}}
-\makeatother
+\renewenvironment{quote}
+ {\list{}{\leftmargin2em\rightmargin0pt}\parindent0pt\parskip0pt\item\relax}
+ {\endlist}
+\renewcommand{\isatagquote}{\begin{quote}}
+\renewcommand{\endisatagquote}{\end{quote}}
+\newcommand{\quotebreak}{\\[1.2ex]}
%% presentation
\setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}
-\pagestyle{headings}
+%% character detail
+\renewcommand{\isadigit}[1]{\isamath{#1}}
\binperiod
\underscoreoff
-\renewcommand{\isadigit}[1]{\isamath{#1}}
-
+%% format
+\pagestyle{headings}
\isabellestyle{it}
--- a/doc-src/Codegen/Thy/Adaption.thy Tue Mar 03 11:00:51 2009 +0100
+++ b/doc-src/Codegen/Thy/Adaption.thy Tue Mar 03 13:20:53 2009 +0100
@@ -323,7 +323,6 @@
instance %quote by default (simp add: eq_bar_def)
end %quote
-
code_type %quotett bar
(Haskell "Integer")
--- a/doc-src/Codegen/Thy/Codegen.thy Tue Mar 03 11:00:51 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,2 +0,0 @@
-
-end
--- a/doc-src/Codegen/Thy/Further.thy Tue Mar 03 11:00:51 2009 +0100
+++ b/doc-src/Codegen/Thy/Further.thy Tue Mar 03 13:20:53 2009 +0100
@@ -79,8 +79,7 @@
*}
datatype %quote form = T | F | And form form | Or form form
-
-ML %quote {*
+ML %quotett {*
fun eval_form @{code T} = true
| eval_form @{code F} = false
| eval_form (@{code And} (p, q)) =
--- a/doc-src/Codegen/Thy/Introduction.thy Tue Mar 03 11:00:51 2009 +0100
+++ b/doc-src/Codegen/Thy/Introduction.thy Tue Mar 03 13:20:53 2009 +0100
@@ -2,8 +2,6 @@
imports Setup
begin
-chapter {* Code generation from @{text "Isabelle/HOL"} theories *}
-
section {* Introduction and Overview *}
text {*
--- a/doc-src/Codegen/Thy/Program.thy Tue Mar 03 11:00:51 2009 +0100
+++ b/doc-src/Codegen/Thy/Program.thy Tue Mar 03 13:20:53 2009 +0100
@@ -287,16 +287,9 @@
@{text case} combinator on queues:
*}
-definition %quote
- aqueue_case_def: "aqueue_case = queue_case"
-
-lemma %quote aqueue_case [code, code inline]:
- "queue_case = aqueue_case"
- unfolding aqueue_case_def ..
-
-lemma %quote case_AQueue [code]:
- "aqueue_case f (AQueue xs ys) = f (ys @ rev xs)"
- unfolding aqueue_case_def AQueue_def by simp
+lemma %quote queue_case_AQueue [code]:
+ "queue_case f (AQueue xs ys) = f (ys @ rev xs)"
+ unfolding AQueue_def by simp
text {*
\noindent The resulting code looks as expected:
@@ -313,8 +306,7 @@
\begin{itemize}
\item When changing the constructor set for datatypes, take care
- to provide an alternative for the @{text case} combinator
- (e.g.~by replacing it using the preprocessor).
+ to provide alternative equations for the @{text case} combinator.
\item Values in the target language need not to be normalised --
different values in the target language may represent the same
--- a/doc-src/Codegen/Thy/Setup.thy Tue Mar 03 11:00:51 2009 +0100
+++ b/doc-src/Codegen/Thy/Setup.thy Tue Mar 03 13:20:53 2009 +0100
@@ -1,12 +1,15 @@
theory Setup
imports Complex_Main
-uses "../../../antiquote_setup.ML" "../../../more_antiquote.ML"
+uses
+ "../../antiquote_setup.ML"
+ "../../more_antiquote.ML"
begin
ML {* no_document use_thys
["Efficient_Nat", "Code_Char_chr", "Product_ord", "~~/src/HOL/Imperative_HOL/Imperative_HOL",
"~~/src/HOL/Decision_Procs/Ferrack"] *}
-ML_val {* Code_Target.code_width := 74 *}
+ML_command {* Code_Target.code_width := 74 *}
+ML_command {* reset unique_names *}
end
--- a/doc-src/Codegen/Thy/document/Adaption.tex Tue Mar 03 11:00:51 2009 +0100
+++ b/doc-src/Codegen/Thy/document/Adaption.tex Tue Mar 03 13:20:53 2009 +0100
@@ -583,7 +583,6 @@
\isanewline
%
\isadelimquotett
-\isanewline
%
\endisadelimquotett
%
--- a/doc-src/Codegen/Thy/document/Further.tex Tue Mar 03 11:00:51 2009 +0100
+++ b/doc-src/Codegen/Thy/document/Further.tex Tue Mar 03 13:20:53 2009 +0100
@@ -154,8 +154,20 @@
%
\isatagquote
\isacommand{datatype}\isamarkupfalse%
-\ form\ {\isacharequal}\ T\ {\isacharbar}\ F\ {\isacharbar}\ And\ form\ form\ {\isacharbar}\ Or\ form\ form\isanewline
+\ form\ {\isacharequal}\ T\ {\isacharbar}\ F\ {\isacharbar}\ And\ form\ form\ {\isacharbar}\ Or\ form\ form%
+\endisatagquote
+{\isafoldquote}%
+%
+\isadelimquote
+%
+\endisadelimquote
\isanewline
+%
+\isadelimquotett
+%
+\endisadelimquotett
+%
+\isatagquotett
\isacommand{ML}\isamarkupfalse%
\ {\isacharverbatimopen}\isanewline
\ \ fun\ eval{\isacharunderscore}form\ %
@@ -181,12 +193,12 @@
\ {\isacharparenleft}p{\isacharcomma}\ q{\isacharparenright}{\isacharparenright}\ {\isacharequal}\isanewline
\ \ \ \ \ \ \ \ eval{\isacharunderscore}form\ p\ orelse\ eval{\isacharunderscore}form\ q{\isacharsemicolon}\isanewline
{\isacharverbatimclose}%
-\endisatagquote
-{\isafoldquote}%
+\endisatagquotett
+{\isafoldquotett}%
%
-\isadelimquote
+\isadelimquotett
%
-\endisadelimquote
+\endisadelimquotett
%
\begin{isamarkuptext}%
\noindent \isa{code} takes as argument the name of a constant; after the
--- a/doc-src/Codegen/Thy/document/Introduction.tex Tue Mar 03 11:00:51 2009 +0100
+++ b/doc-src/Codegen/Thy/document/Introduction.tex Tue Mar 03 13:20:53 2009 +0100
@@ -18,10 +18,6 @@
%
\endisadelimtheory
%
-\isamarkupchapter{Code generation from \isa{Isabelle{\isacharslash}HOL} theories%
-}
-\isamarkuptrue%
-%
\isamarkupsection{Introduction and Overview%
}
\isamarkuptrue%
--- a/doc-src/Codegen/Thy/document/Program.tex Tue Mar 03 11:00:51 2009 +0100
+++ b/doc-src/Codegen/Thy/document/Program.tex Tue Mar 03 13:20:53 2009 +0100
@@ -573,7 +573,7 @@
\endisadelimquote
%
\begin{isamarkuptext}%
-\noindent Here we define a \qt{constructor} \isa{Program{\isachardot}AQueue} which
+\noindent Here we define a \qt{constructor} \isa{AQueue} which
is defined in terms of \isa{Queue} and interprets its arguments
according to what the \emph{content} of an amortised queue is supposed
to be. Equipped with this, we are able to prove the following equations
@@ -628,22 +628,11 @@
\endisadelimquote
%
\isatagquote
-\isacommand{definition}\isamarkupfalse%
-\isanewline
-\ \ aqueue{\isacharunderscore}case{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}aqueue{\isacharunderscore}case\ {\isacharequal}\ queue{\isacharunderscore}case{\isachardoublequoteclose}\isanewline
-\isanewline
\isacommand{lemma}\isamarkupfalse%
-\ aqueue{\isacharunderscore}case\ {\isacharbrackleft}code{\isacharcomma}\ code\ inline{\isacharbrackright}{\isacharcolon}\isanewline
-\ \ {\isachardoublequoteopen}queue{\isacharunderscore}case\ {\isacharequal}\ aqueue{\isacharunderscore}case{\isachardoublequoteclose}\isanewline
+\ queue{\isacharunderscore}case{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
+\ \ {\isachardoublequoteopen}queue{\isacharunderscore}case\ f\ {\isacharparenleft}AQueue\ xs\ ys{\isacharparenright}\ {\isacharequal}\ f\ {\isacharparenleft}ys\ {\isacharat}\ rev\ xs{\isacharparenright}{\isachardoublequoteclose}\isanewline
\ \ \isacommand{unfolding}\isamarkupfalse%
-\ aqueue{\isacharunderscore}case{\isacharunderscore}def\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
-\isanewline
-\isanewline
-\isacommand{lemma}\isamarkupfalse%
-\ case{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
-\ \ {\isachardoublequoteopen}aqueue{\isacharunderscore}case\ f\ {\isacharparenleft}AQueue\ xs\ ys{\isacharparenright}\ {\isacharequal}\ f\ {\isacharparenleft}ys\ {\isacharat}\ rev\ xs{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\ \ \isacommand{unfolding}\isamarkupfalse%
-\ aqueue{\isacharunderscore}case{\isacharunderscore}def\ AQueue{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
+\ AQueue{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
\ simp%
\endisatagquote
{\isafoldquote}%
@@ -708,8 +697,7 @@
\begin{itemize}
\item When changing the constructor set for datatypes, take care
- to provide an alternative for the \isa{case} combinator
- (e.g.~by replacing it using the preprocessor).
+ to provide alternative equations for the \isa{case} combinator.
\item Values in the target language need not to be normalised --
different values in the target language may represent the same
@@ -1098,7 +1086,7 @@
%
\begin{isamarkuptext}%
\noindent In the corresponding code, there is no equation
- for the pattern \isa{Program{\isachardot}AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}}:%
+ for the pattern \isa{AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}}:%
\end{isamarkuptext}%
\isamarkuptrue%
%
--- a/doc-src/Codegen/codegen.tex Tue Mar 03 11:00:51 2009 +0100
+++ b/doc-src/Codegen/codegen.tex Tue Mar 03 13:20:53 2009 +0100
@@ -1,5 +1,5 @@
-\documentclass[12pt,a4paper,fleqn]{report}
+\documentclass[12pt,a4paper,fleqn]{article}
\usepackage{latexsym,graphicx}
\usepackage[refpage]{nomencl}
\usepackage{../iman,../extra,../isar,../proof}
@@ -23,7 +23,7 @@
\maketitle
\begin{abstract}
- This tutorial gives an introduction to a generic code generator framework in Isabelle
+ \noindent This tutorial gives an introduction to a generic code generator framework in Isabelle
for generating executable code in functional programming languages from logical
specifications in Isabelle/HOL.
\end{abstract}
--- a/doc-src/Codegen/style.sty Tue Mar 03 11:00:51 2009 +0100
+++ b/doc-src/Codegen/style.sty Tue Mar 03 13:20:53 2009 +0100
@@ -3,6 +3,9 @@
\newcommand{\tocentry}[1]{\cleardoublepage\phantomsection\addcontentsline{toc}{chapter}{#1}
\@mkboth{\MakeUppercase{#1}}{\MakeUppercase{#1}}}
+%% paragraphs
+\setlength{\parindent}{1em}
+
%% references
\newcommand{\secref}[1]{\S\ref{#1}}
@@ -16,17 +19,18 @@
%% verbatim text
\newcommand{\isatypewriter}{\fontsize{9pt}{0pt}\tt\renewcommand{\baselinestretch}{1}\setlength{\baselineskip}{9pt}}
-%% quoted segments
-\makeatletter
+%% quote environment
\isakeeptag{quote}
-\newenvironment{quotesegment}{\begin{quote}\isa@parindent\parindent\parindent0pt\isa@parskip\parskip\parskip0pt}{\end{quote}}
-\renewcommand{\isatagquote}{\begin{quotesegment}}
-\renewcommand{\endisatagquote}{\end{quotesegment}}
-\makeatother
+\renewenvironment{quote}
+ {\list{}{\leftmargin2em\rightmargin0pt}\parindent0pt\parskip0pt\item\relax}
+ {\endlist}
+\renewcommand{\isatagquote}{\begin{quote}}
+\renewcommand{\endisatagquote}{\end{quote}}
+\newcommand{\quotebreak}{\\[1.2ex]}
\isakeeptag{quotett}
-\renewcommand{\isatagquotett}{\begin{quotesegment}\isabellestyle{tt}\isastyle}
-\renewcommand{\endisatagquotett}{\end{quotesegment}\isabellestyle{it}\isastyle}
+\renewcommand{\isatagquotett}{\begin{quote}\isabellestyle{tt}\isastyle}
+\renewcommand{\endisatagquotett}{\end{quote}\isabellestyle{it}\isastyle}
%% a trick
\newcommand{\isasymSML}{SML}
@@ -34,11 +38,14 @@
%% presentation
\setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}
-\pagestyle{headings}
+%% character detail
+\renewcommand{\isadigit}[1]{\isamath{#1}}
\binperiod
\underscoreoff
-\renewcommand{\isadigit}[1]{\isamath{#1}}
+%% format
+\pagestyle{headings}
+\isabellestyle{it}
%% ml reference
\newenvironment{mldecls}{\par\noindent\begingroup\footnotesize\def\isanewline{\\}\begin{tabular}{l}}{\end{tabular}\smallskip\endgroup}