summaryrefslogtreecommitdiff
path: root/macros/latex/contrib/stex/sty/statements/statements.dtx
diff options
context:
space:
mode:
Diffstat (limited to 'macros/latex/contrib/stex/sty/statements/statements.dtx')
-rw-r--r--macros/latex/contrib/stex/sty/statements/statements.dtx1304
1 files changed, 0 insertions, 1304 deletions
diff --git a/macros/latex/contrib/stex/sty/statements/statements.dtx b/macros/latex/contrib/stex/sty/statements/statements.dtx
deleted file mode 100644
index 3d839be5fb..0000000000
--- a/macros/latex/contrib/stex/sty/statements/statements.dtx
+++ /dev/null
@@ -1,1304 +0,0 @@
-% \iffalse meta-comment
-% An Infrastructure for Mathematical Statements in sTeX
-% Copyright (C) 2004-2008 Michael Kohlhase, all rights reserved
-% this file is released under the
-% LaTeX Project Public License (LPPL)
-%
-% The original of this file is in the public repository at
-% http://github.com/KWARC/sTeX/
-% \fi
-%
-% \iffalse
-%<package>\NeedsTeXFormat{LaTeX2e}[1999/12/01]
-%<package>\ProvidesPackage{statements}[2019/03/20 v1.4 Semantic Markup for Statements]
-%
-%<*driver>
-\documentclass{ltxdoc}
-\usepackage[utf8]{inputenc}
-\usepackage[T1]{fontenc}
-\usepackage{url,array,float,amsfonts}
-\usepackage{statements,presentation}
-\usepackage{paralist}
-\usepackage[show]{ed}
-\usepackage[hyperref=auto,style=alphabetic]{biblatex}
-\addbibresource{kwarcpubs.bib}
-\addbibresource{extpubs.bib}
-\addbibresource{kwarccrossrefs.bib}
-\addbibresource{extcrossrefs.bib}
-\usepackage{stex-logo}
-\usepackage{ctangit}
-\usepackage{hyperref}
-\makeindex
-\floatstyle{boxed}
-\newfloat{exfig}{thp}{lop}
-\floatname{exfig}{Example}
-\def\githubissue#1{\cite{sTeX:github:on}, \hyperlink{https://github.com/KWARC/sTeX/issues/#1}{issue #1}}
-\begin{document}
-\RecordChanges
-\DocInput{statements.dtx}
-\end{document}
-%</driver>
-% \fi
-%
-% \CheckSum{809}
-%
-% \changes{v0.9}{2005/06/14}{First Version with Documentation}
-% \changes{v0.9a}{2005/07/01}{Completed Documentation}
-% \changes{v0.9b}{2005/08/06}{Complete functionality and Updated Documentation}
-% \changes{v0.9c}{2006/01/13}{more packaging}
-% \changes{v0.9d}{2007/09/09}{moved omtext and friends to the omdoc package}
-% \changes{v0.9d}{2007/09/09}{made dependence on the omdoc package explicit}
-% \changes{v0.9d}{2007/09/09}{adding ids to many elements}
-% \changes{v0.9e}{2008/05/27}{adding cross-references}
-% \changes{v0.9e}{2008/09/29}{augmenting the index macros with optional values}
-% \changes{v0.9f}{2008/12/04}{changed 'consymb' to 'symboldec' and documented it.}
-% \changes{v0.9g}{2010/01/14}{the package is now based on {\texttt{ntheorem for presentation}}}
-% \changes{v0.9g}{2010/01/19}{Added support for localization}
-% \changes{v0.9g}{2010/02/23}{added {\texttt{\textbackslash symref}}}
-% \changes{v1.0}{2010/06/18}{now based on {\texttt{omtext}} package instead of {\texttt{omdoc}}}
-% \changes{v1.0}{2010/07/13}{adding {\texttt{\textbackslash inlineex}}}
-% \changes{v1.1}{2011/08/25}{renaming all convenience macros for {\texttt{\textbackslash
-% definendum}} and {\texttt{\textbackslash termref}}}
-% \changes{v1.1}{2012/07/06}{adding \texttt{\textbackslash usevocab} to example for importing}
-% \changes{v1.1}{2013/05/17}{more support for types: \texttt{typedec} and
-% \texttt{\textbackslash inlinetypedec}}
-% \changes{v1.2}{2015/04/03}{adding optional last arg to \texttt{\textbackslash \*defi*}}
-% \changes{v1.2}{2015/04/17}{adding \texttt{\textbackslash inlineass}}
-% \changes{v1.2}{2015/09/05}{adding \texttt{\textbackslash defis} and friends}
-% \changes{v1.3}{2017/07/31}{adding \texttt{\textbackslash Defi}, \texttt{\textbackslash Trefi} and friends}
-% \changes{v1.4}{2017/10/15}{changing the optional argument of \texttt{\textbackslash
-% defi} and friends to a keyval argument}
-%
-% \GetFileInfo{statements.sty}
-%
-% \MakeShortVerb{\|}
-% \def\scsys#1{{{\sc #1}}\index{#1@{\sc #1}}}
-% \def\xml{\scsys{Xml}}
-% \def\mathml{\scsys{MathML}}
-% \def\omdoc{\scsys{OMDoc}}
-% \def\openmath{\scsys{OpenMath}}
-% \def\latexml{\scsys{LaTeXML}}
-% \def\perl{\scsys{Perl}}
-% \def\activemath{\scsys{ActiveMath}}
-% \title{Semantic Markup for Mathematical Statements\thanks{Version {\fileversion} (last revised
-% {\filedate})}}
-% \author{Michael Kohlhase\\
-% FAU Erlangen-N\"urnberg\\
-% \url{http://kwarc.info/kohlhase}}
-% \maketitle
-%
-% \begin{abstract}
-% The |statements| package is part of the {\stex} collection, a version of {\TeX/\LaTeX}
-% that allows to markup {\TeX/\LaTeX} documents semantically without leaving the
-% document format, essentially turning {\TeX/\LaTeX} into a document format for
-% mathematical knowledge management (MKM).
-%
-% This package provides semantic markup facilities for mathematical statements like
-% Theorems, Lemmata, Axioms, Definitions, etc. in {\stex} files. This structure can be
-% used by MKM systems for added-value services, either directly from the {\sTeX}
-% sources, or after translation.
-% \end{abstract}
-%
-% \setcounter{tocdepth}{2}\tableofcontents\newpage
-%
-% \section{Introduction}\label{sec:intro}
-%
-% The motivation for the |statements| package is very similar to that for semantic macros
-% in the |modules| package: We want to annotate the structural semantic properties of
-% statements in the source, but present them as usual in the formatted documents. In
-% contrast to the case for mathematical objects, the repertoire of mathematical statements
-% and their structure is more or less fixed.
-%
-% This structure can be used by MKM systems for added-value services, either directly from
-% the {\sTeX} sources, or after translation. Even though it is part of the {\stex}
-% collection, it can be used independently, like it's sister package |sproofs|.
-%
-% {\stex}~\cite{Kohlhase:ulsmf08,sTeX:online} is a version of {\TeX/\LaTeX} that allows to
-% markup {\TeX/\LaTeX} documents semantically without leaving the document format,
-% essentially turning {\TeX/\LaTeX} into a document format for mathematical knowledge
-% management (MKM). Currently the {\omdoc} format~\cite{Kohlhase:OMDoc1.2} is directly
-% supported.
-%
-% \section{The User Interface}\label{sec:user-interface}
-%
-% The |statements| package supplies a semantically oriented infrastructure for marking up
-% mathematical statements: fragments of natural language that state properties of
-% mathematical objects, e.g. axioms, definitions, or theorems. The |statement| package
-% provides an infrastructure for marking up the semantic relations between statements for
-% the {\omdoc} transformation and uses the |ntheorem| package~\cite{MaySch:eltte09} for
-% formatting (i.e. transformation to PDF).
-%
-% \subsection{Package Options}\label{sec:user:options}
-%
-% The |statements| package provides the \DescribeMacro{defindex}|defindex| option to
-% \sTeX. If this is set, then definienda are automatically passed into the index of the
-% document. Furthermore, the |statements| package passes the
-% \DescribeMacro{showmeta}|showmeta| to the |metakeys| package. If this is set, then the
-% metadata keys are shown (see~\cite{Kohlhase:metakeys:ctan} for details and customization
-% options). The |nontheorem| option tells statements not to load the |ntheorem| package --
-% in case some other theorem package is already loaded; e.g. by the |beamer| package and
-% we prefer that. Note that using the |nontheorem| option in a case where no theorem
-% package is loaded will lead to errors.
-%
-% \subsection{Statements}\label{sec:statements}
-%
-% All the statements are marked up as environments, that take a |KeyVal| argument that
-% allows to annotate semantic information. Generally, we distinguish two forms of
-% statements:
-% \begin{description}
-% \item[{\twintoo{block}{statement}s}] have explicit discourse markers that delimit their
-% content in the surrounding text, e.g. the boldface word ``{\bf{Theorem}:}'' as a start
-% marker and a little line-end box as an end marker of a proof.
-% \item[{\twintoo{flow}{statement}s}] do not have explicit markers, they are interspersed
-% with the surrounding text.
-% \end{description}
-% Since they have the same semantic status, they must both be marked up, but styled
-% differently. We distinguish between these two presentational forms with the
-% \DescribeMacro{display=}|display| key, which is allowed on all statement
-% environments. If it has the value |block| (the default), then the statement will be
-% presented in a paragraph of its own, have explicit discourse markers for its begin and
-% end, possibly numbering, etc. If it has the value |flow|, then no extra presentation
-% will be added the semantic information is invisible to the reader. Another key that is
-% present on all statement environments in the \DescribeMacro{id=}|id| key it allows to
-% identify the statement with a name and to reference it with the semantic referencing
-% infrastructure provided by the |sref| package~\ctancite{Kohlhase:sref}.
-%
-% \subsubsection{Axioms and Assertions}\label{sec:user:axiomassertion}
-%
-% The \DescribeEnv{assertion}|assertion| environment is used for marking up statements
-% that can be justified from previously existing knowledge (usually marked with the
-% monikers ``Theorem'', ``Lemma'', ``Proposition'', etc. in mathematical vernacular). The
-% environment |assertion| is used for all of them, and the particular subtype of
-% assertion is given in the \DescribeMacro{type=}|type| key. So instead of
-% |\begin{Lemma}|\iffalse\end{Lemma}\fi we have to write
-% |\begin{assertion}[type=lemma]|\iffalse\end{assertion}\fi (see
-% Example~\ref{fig:assertion} for an example).
-% \begin{exfig}
-% \begin{verbatim}
-% \begin{assertion}[id=sum-over-odds,type=lemma]
-% $\sum_{i=1}^n{2i-1}=n^2$
-% \end{assertion}
-% \end{verbatim}
-% \vspace{-1em}will lead to the result\vspace{-2em}\par\noindent
-% \begin{assertion}[id=sum-over-odds,type=lemma]
-% $\sum_{i=1}^n{2i-1}=n^2$
-% \end{assertion}
-% \caption{Semantic Markup for a Lemma in a {\texttt{module}} context}\label{fig:assertion}
-% \end{exfig}
-%
-% Whether we will see the keyword ``Lemma'' will depend on the value of the optional
-% |display| key. In all of the |assertion| environments, the presentation expectation is
-% that the text will be presented in italic font. The presentation (keywords, spacing, and
-% numbering) of the |assertion| environment is delegated to a theorem styles from the
-% |ntheorem| environment. For an assertion of type \meta{type} the |assertion| environment
-% calls the |ST|\meta{type}|AssEnv| environment provided by the |statements| package; see
-% Figure~\ref{fig:assertion-types} for a list of provided assertion types. Their
-% formatting can be customized by redefining the |ST|\meta{type}|AssEnv| environment via
-% the |\renewtheorem| command from the |ntheorem| package; see~\cite{MaySch:eltte09} for
-% details.
-%
-% \begin{exfig}
-% \begin{tabular}{|l|l|}\hline
-% Value & Explanation \\\hline\hline
-% \textbf{theorem}, \textbf{proposition}
-% & an important assertion with a proof\\\hline
-% \multicolumn{2}{|p{12cm}|}{\footnotesize Note that the meaning of \textbf{theorem}
-% (in this case the existence of a proof) is not
-% enforced by {\omdoc} applications. It can be appropriate to give an assertion
-% the \textbf{theorem}, if the
-% author knows of a proof (e.g. in the literature), but has not formalized it in
-% {\omdoc} yet.}\\\hline\hline
-% \textbf{lemma} & a less important assertion with a proof\\\hline
-% \multicolumn{2}{|p{12cm}|}{\footnotesize The difference of importance specified
-% here is even softer than the other ones, since e.g. reusing
-% a mathematical paper as a chapter in a larger monograph, may make it necessary to
-% downgrade a theorem (e.g. the main theorem of the paper) and give it the status of
-% a lemma in the overall work.}\\\hline\hline
-% \textbf{corollary} & a simple consequence\\\hline
-% \multicolumn{2}{|p{12cm}|}{\footnotesize An assertion is
-% sometimes marked as a corollary to some other statement, if the proof is
-% considered simple. This is often the case for important theorems that are simple
-% to get from technical lemmata.}\\\hline\hline
-% \textbf{postulate}, \textbf{conjecture}
-% & an assertion without proof or counter-exam\-ple\\\hline
-% \multicolumn{2}{|p{12cm}|}{\footnotesize Conjectures are assertions, whose
-% semantic value is not yet decided, but which the author considers likely to be
-% true. In particular, there is no proof or counter-example.}\\\hline\hline
-% \textbf{false-conjecture}
-% & an assertion with a counter-example\\\hline
-% \multicolumn{2}{|p{12cm}|}{\footnotesize A conjecture that has proven to be false,
-% i.e. it has a counter-example. Such assertions are often kept for illustration and
-% historical purposes.}\\\hline\hline
-% \textbf{obligation}, \textbf{assumption}
-% & an assertion on which a proof of another depends\\\hline
-% \multicolumn{2}{|p{12cm}|}{\footnotesize These kinds of assertions
-% are convenient during the exploration of a mathematical theory. They can be used
-% and proven later (or assumed as an axiom).}\\\hline\hline
-% \textbf{rule}
-% & a normative assertion\\\hline
-% \multicolumn{2}{|p{12cm}|}{\footnotesize These kinds of assertions can be interpreted
-% procedurally to trigger actions}\\\hline\hline
-% \textbf{observation}, \textbf{remark} & if everything else fails\\\hline
-% \multicolumn{2}{|p{12cm}|}{\footnotesize This type is the catch-all if none of the others
-% applies.}\\\hline
-% \end{tabular}
-% \caption{Types of Mathematical Assertions}\label{fig:assertion-types}
-% \end{exfig}
-%
-% \DescribeEnv{axiom} The |axiom| environment is similar to |assertion|, but the content
-% has a different ontological status: axioms are assumed without (formal) justification,
-% whereas assertions are expected to be justified from other assertions, axioms or
-% definitions. This environment relegates the formatting to the |STaxiomEnv| environment,
-% which can be redefined for configuration.
-%
-% \subsubsection{Symbols}\label{sec:user:symbol}
-%
-% \DescribeEnv{symboldec} The |symboldec| environment can be used for declaring concepts
-% and symbols. Note the the |symdef| forms from the |modules| package will not do this
-% automatically (but the |definition| environment and the |\inlinedef| macro will for all
-% the definienda; see below). The |symboldec| environment takes an optional keywords
-% argument with the keys |id|, |role|, |title| and |name|. The first is for general
-% identification, the |role| specifies the {\openmath}/{\omdoc} role, which is one of
-% |object|, |type|, |sort|, |binder|, |attribution|, |application|, |constant|,
-% |semantic-attribution|, and |error| (see the {\omdoc} specification for details). The
-% |name| key specifies the {\openmath} name of the symbol, it should coincide with the
-% control sequence introduced by the corresponding |\symdef| (if one is present). The
-% |title| key is for presenting the title of this symbol as in other statements. Usually,
-% |axiom| and |symboldec| environments are used together as in Figure~\ref{fig:axioms}.
-%
-%\begin{exfig}
-% \begin{verbatim}
-% \symdef{zero}{0}
-% \begin{symboldec}[name=zero,title=The number zero,type=constant]
-% The number zero, it is used as the base case of the inductive definition
-% of natural numbers via the Peano Axioms.
-% \end{symboldec}
-%
-% \symdef{succ}[1]{\prefix{s}{#1}}
-% \begin{symboldec}[name=succ,title=The Successor Function,type=application]
-% The successor function, it is used for the step case of the inductive
-% definition of natural numbers via the Peano Axioms.
-% \end{symboldec}
-%
-% \symdef{NaturalNumbers}{\mathbb{N}}
-% \begin{symboldec}[name=succ,title=The Natural Numbers,type=constant]
-% The natural numbers inductively defined via the Peano Axioms.
-% \end{symboldec}
-%
-% \begin{axiom}[id=peano.P1,title=P1]
-% $\zero$ is a natural number.
-% \end{axiom}
-% ...
-% \begin{axiom}[id=peano.P5,title=P5]
-% Any property $P$ such $P(\zero)$ and $P(\succ{k})$ whenever $P(k)$
-% holds for all $n$ in $\NaturalNumbers$
-% \end{axiom}
-% \end{verbatim}
-% \vspace{-1em}will lead to the result\medskip\par\noindent
-% \begin{module}[id=peano]
-% \symdef{zero}{0}
-% \begin{symboldec}[name=zero,title=The number zero,role=constant]
-% The number zero, it is used as the base case of the inductive definition
-% of natural numbers via the Peano Axioms.
-% \end{symboldec}
-%
-% \symdef{succ}[1]{\prefix{s}{#1}}
-% \begin{symboldec}[name=succ,title=The Successor Function,role=application]
-% The successor function, it is used for the step case of the inductive
-% definition of natural numbers via the Peano Axioms.
-% \end{symboldec}
-%
-% \symdef{NaturalNumbers}{\mathbb{N}}
-% \begin{symboldec}[name=succ,title=The Natural Numbers,role=constant]
-% The natural numbers inductively defined via the Peano Axioms.
-% \end{symboldec}
-%
-% \begin{axiom}[id=peano.P1,title=P1]
-% $\zero$ is a natural number.
-% \end{axiom}
-% \ldots \stepcounter{STtheoremAssEnv}\stepcounter{STtheoremAssEnv}\stepcounter{STtheoremAssEnv}
-% \begin{axiom}[id=peano.P5,title=P5]
-% Any property $P$ such $P(\zero)$ and $P(\succ{k})$ whenever $P(k)$
-% holds for all $n$ in $\NaturalNumbers$
-% \end{axiom}
-% \end{module}
-% \caption{Semantic Markup for the Peano Axioms}\label{fig:axioms}
-% \end{exfig}
-%
-% \subsubsection{Types}\label{sec:user:types}
-%
-% In many cases, we can give additional information for symbols in the form of type
-% assignments. \sTeX does not fix a type system, but allows types to be arbitrary
-% mathematical objects that they can be defined in (imported) modules. The
-% \DescribeMacro{\symtype}|\symtype| macro can be used to assign a type to a symbol:
-% \begin{quote}
-% |\symtype[|\meta{keys}|]{|\meta{sym}|}{|\meta{type}|}|
-% \end{quote}
-% assigns the type \meta{type} to a symbol with name \meta{sym}. For instance
-%
-% \begin{center}%
-% |\symtype[id=plus-nat.type,system=sts]{plus}{\fntype{\Nat,\Nat}\Nat}|
-% \end{center}
-%
-% \noindent assigns the type $\mathbb{N}\times\mathbb{N}\rightarrow\mathbb{N}$ (in the
-% |sts| type system) to the symbol |plus|. This states (type assignments are statements
-% epistemologically) that addition is a binary function on natural numbers. The |\symtype|
-% macro supports the keys |id| (for identifiers) and |system| for the type system.
-%
-% Often, type assignments occur in informal context, where the type assignment is given by
-% a natural language sentence or phrase. For this, the |statements| package supplies the
-% \DescribeEnv{typedec}|typedec| environment and the
-% \DescribeMacro{\inlinetypedec}|\inlinetypedec| macro. Both take an optional keyval
-% argument followed by the type. The phrase/sentence is the body of the |typedec|
-% environment and the last argument of the |\inlinetypedec| macro. The symbol name is
-% given in via the |for| key. For convenience, the macro
-% \DescribeMacro{\thedectype}|\thedectype| is bound to the type. So we can use
-%\begin{verbatim}
-% \begin{typedec}[for=plus,id=plus-nat.type]{\fntype{\Nat,\Nat}\Nat}
-% $+:\thedectype$ is a binary function on $\Nat$
-% \end{typedec}
-% \end{verbatim}
-% instead of the |\symtype| above in an informal setting.
-%
-% \subsubsection{Definitions, and Definienda}\label{sec:definition}
-%
-% \DescribeEnv{definition} The |definition| environment is used for marking up
-% mathematical definitions. Its peculiarity is that it defines (i.e. gives a meaning to)
-% new mathematical concepts or objects. These\DescribeMacro{\definiendum} are identified
-% by the |\definiendum| macro, which is used as
-% |\definiendum[|\meta{keys}|]{|\meta{text}|}|. Here, \meta{text} is the text that is to
-% be emphasized in the presentation. |\definiendum| takes the key
-% \DescribeMacro{name}|name| for the optional system name of the symbol defined (for
-% reference via |\termref|, see Section~\ref{sec:user:crossref}). If the |name| key is not
-% given, then \meta{text} is used as a system name instead, which is usually sufficient
-% for most situations. The set of keys is extensible to add additional metadata for the
-% definiendum. Currently only the \DescribeMacro{lemma}|lemma| key is supported, which
-% allows to specify the base form of the name of the concept involved -- e.g. for
-% referencing in a glossary or index.
-%
-%\begin{exfig}
-% \def\succ#1{s(#1)}
-% \begin{verbatim}
-% \symdef{one}{1}
-% \begin{definition}[id=one.def,for=one]
-% $\notatiendum[one]{\one}$ is the successor of $\zero$
-% (formally: $\one :=\succ\zero$)
-% \end{definition}
-% \end{verbatim}
-% \vspace{-1em}will lead to the result\medskip\par\noindent\vspace*{-1em}
-% \begin{module}[id=onedef]
-% \importmodule{peano}
-% \symdef{one}{1}
-% \begin{definition}[id=one.def,for=one]
-% $\notatiendum[one]{\one}$ is the successor of $\zero$
-% (formally: $\one :=\succ\zero$)
-% \end{definition}
-% \end{module}
-% \caption{A Definition based on Figure {\ref{fig:axioms}}}\label{fig:definition}
-% \end{exfig}
-% The \DescribeMacro{defi}|\defi{|\meta{word}|}| macro combines the functionality of the
-% |\definiendum| macro with index markup from the |omdoc|
-% package~\ctancite{Kohlhase:smomdl}: For definienda where the lemma and \meta{text}
-% coincide use
-% \begin{center}
-% |\defi[|\meta{name}|]{|\meta{lemma}|}[|\meta{indexkeys}|]|
-% \end{center}
-% to markup a definiendum \meta{lemma} with system name \meta{name} that appear in the
-% index (where \meta{indexkeys} are passed to the |\omdoc@index*| macros from the |omtext|
-% package) --- in other words in almost all definitions of single-word concepts. We also
-% have the variants \DescribeMacro{\defii}|\defii|, \DescribeMacro{\defiii}|\defiii|, and
-% \DescribeMacro{\defiv}|\defiv| for (adjectivized) multi-word compounds. Note that if
-% the definiendum contains semantic macros, then we need to specify the |loadmodules| key
-% and also protect the semantic macro. For instance if |\eset| is the semantic macro for
-% $\emptyset$, then we would use
-% \begin{verbatim}
-% \defii[eset-comp]{$\protect\eset$}{compatible}[loadmodules]
-% \end{verbatim}
-% for the definiendum markup.
-%
-% \begin{exfig}
-% \begin{verbatim}
-% A \defi{graph} consists of \adefi{vertices}{vertex} and \defis{edge}.
-% \end{verbatim}
-% \caption{Definienda where Lemma and Text Form differ}\label{fig:lemma}
-% \end{exfig}
-%
-% For the cases where the lemma and \meta{text} are different we can use the variants
-% \DescribeMacro{\adefi}|\adefi|, \DescribeMacro{\adefii}|\adefii|,
-% \DescribeMacro{\adefiii}|\adefiii|, and \DescribeMacro{\adefiv}|\adefiv| that have
-% an additional first argument that allows to specify an alternative \meta{text}; see
-% Figure~\ref{fig:defin}. The main use of these is to mark up inflected forms as in
-% Figure~\ref{fig:lemma}.
-%
-% As the greatest number of these are plurals, which tends to be regular (e.g. adding a
-% trailing ``s'' in English), we provide the variants \DescribeMacro{\defis}|\defis|,
-% \DescribeMacro{\defiis}|\defiis|, \DescribeMacro{\defiiis}|\defiiis|, and
-% \DescribeMacro{\defivs}|\defivs| for that case: |\defiis{simple}{group}| is
-% equivalent to much longer |\adefii{simple groups}{simple}{group}| (but also see
-% Figure~\ref{fig:lemma}).
-%
-% \begin{exfig}
-% \begin{tabular}{l|l|l}
-% \multicolumn{3}{l}{source}\\\hline
-% system name & result & index \\\hline\hline
-% \multicolumn{3}{l}{\texttt{\textbackslash defi\{concept\}}}\\\hline
-% |concept| & concept& concept\\\hline\hline
-% \multicolumn{3}{l}{\texttt{\textbackslash defi[csymbol]\{concept\}}}\\\hline
-% |csymbol| & concept & concept\\\hline\hline
-% \multicolumn{3}{l}{\texttt{\textbackslash adefi[csymbol]\{concepts\}\{concept\}}}\\\hline
-% |csymbol| & concepts & concept\\\hline\hline
-% \multicolumn{3}{l}{\texttt{\textbackslash defii\{concept\}\{group\}}}\\\hline
-% |concept-group| & concept group & concept group, \\
-% && group - , concept\\\hline\hline
-% \multicolumn{3}{l}{\texttt{\textbackslash adefii\{small\}\{concept\}\{group\}}}\\\hline
-% |small-concept-group| & small concept group & small concept group, \\
-% && concept group - , small\\\hline
-% \end{tabular}
-% \caption{Some definienda with Index}\label{fig:defin}
-% \end{exfig}
-%
-% Note that the |\definiendum|, |\defi*|, |\adefi*|, and |\defi*s|, macros can only be
-% used inside the definitional situation, i.e. in a |definition| or |symboldec|
-% environment or a |\inlinedef| macro. If you find yourself in a situation where you want
-% to use it outside, you will most likely want to wrap the appropriate text fragment in a
-% |\begin{definition}[display=flow]| ... and |\end{definition}|. For instance, we could
-% continue the example in Figure~\ref{fig:axioms} with the |definition| environment in
-% Figure~\ref{fig:definition}.
-%
-% \DescribeMacro{\inlinedef} Sometimes we define mathematical concepts in passing, e.g. in
-% a phrase like ``\ldots $s(o)$ which we call {\textbf{one}}.''. For this we cannot use
-% the |definition| environment, which presupposes that its content gives all that is
-% needed to understand the definition. But we do want to make use of the infrastructure
-% introduced for the |definition| environment. In this situation, we just wrap the phrase
-% in an |\inlinedef| macro that makes them available. The |\inlinedef| macro accepts the
-% same |id| and |for| keys in its optional argument, and additionally the |verbalizes| key
-% which can be used to point to a full definition of the concept somewhere else.
-%
-% Note that definienda can only be referenced via a |\term| element, if they are only
-% allowed inside a named module, i.e. a |module| environment with a name given by the
-% |id=| key or the |theory=| key on is specified on the definitional environment.
-%
-% \subsubsection{Examples}\label{sec:user:example}
-%
-% \DescribeEnv{example} The |example| environment is a generic statement environment,
-% except that the |for| key should be given to specify the identifier what this is an
-% example for. The |example| environment also expects a |type| key to be specified, so
-% that we know whether this is an example or a counterexample.
-%
-% \DescribeMacro{\inlineex} The |\inlineex| is analogous to |\inlinedef|, only that it is
-% used for inline examples, e.g. ``\ldots mammals, e.g. goats''. Note that we have used an
-% inline example for an inline example.
-%
-%
-% \subsection{Cross-Referencing Symbols and Concepts}\label{sec:user:crossref}
-%
-% If we have defined a concept with the |\definiendum| macro, then we can mark up other
-% occurrences of the term as referring to this concept. Note that this process cannot be
-% fully automatized yet, since that would need advanced language technology to get around
-% problems of disambiguation, inflection, and non-contiguous phrases\footnote{We do have a
-% program that helps annotate larger text collections spotting the easy cases; see
-% {\url{http://kwarc.info/projects/stex}} and look for the program
-% |termin|.}. Therefore, the \DescribeMacro{\termref}|\termref| can be used to make this
-% information explicit. It takes the keys
-% \begin{compactdesc}
-% \item[\texttt{cdbase}] to specify a URI (a path actually, since {\LaTeX} cannot load
-% from URIs) where the module can be found.
-% \item[\texttt{cd}] to specify the module in which the term is defined. If the |cd| key
-% is not given, then the current module is assumed. If no |cdbase| is specified (this is
-% the usual case), then the CD has to be imported via a |\importmodule| from the
-% |modules| package~\ctancite{KohAmb:smmssl}.
-% \item[\texttt{name}] to specify the name of the definiendum (which is given in the body
-% of the |\definiendum| or the optional argument). If the |name| key is not specified,
-% then argument of the |\termref| macro is used.
-% \item[\texttt{role}] is currently unused.
-% \end{compactdesc}
-% |\termref[cd=|\meta{cd}|,name=|\meta{name}|]{|\meta{text}|}| will just typeset the link
-% text \meta{text} with (if the |hyperref| package is loaded) a hyperlink to the
-% definition in module \meta{cd} that defines the concept \meta{name}, e.g. that contains
-% |\defi[|\meta{name}|]{|\meta{text}|}|.
-%
-% Just as the |\definiendum| macro has the convenience variants |\defi| and |\?defi*|, the
-% |\termref| has variants |\trefi|, |\trefii|, |\trefiii|, and |\trefiv| that take two and
-% three arguments for the parts of the compositum. In the same module, concepts that are
-% marked up by |\defi{|\meta{name}|}| in the definition can be referenced by
-% \DescribeMacro{\trefi}|\trefi{|\meta{name}|}|. Here the link text is just
-% \meta{name}. Concepts defined via |\defii{|\meta{first}|}{|\meta{second}|}| can be
-% referenced by \DescribeMacro{\trefii}|\trefii{|\meta{first}|}{|\meta{second}|}| (with
-% link text ``\meta{first} \meta{second}'') and analogously for
-% |\defiii|/\DescribeMacro{\trefiii}|\trefiii| and % |\defiv|/\DescribeMacro{\trefiv}|\trefiv|.
-%
-% We have variants \DescribeMacro{\atref*}|\atrefi|, |\atrefii|, |\atrefiii|, and
-% |\atrefiv| with alternative link text. For instance
-% |\atrefii{|\meta{text}|{|\meta{first}|}{|\meta{second}|}| references a concept
-% introduced by |\defii{|\meta{first}|}{|\meta{second}|}| but with link text \meta{text}.
-% Of course, if the system identifier is given explicitly in the optional argument of the
-% definition form, as in |\defii[|\meta{name}|]{|\meta{first}|}{|\meta{second}|}|, then
-% the terms are referenced by |\trefi{|\meta{name}|}|.
-%
-% For referencing terms outside the current module, the module name can be specified in
-% the first optional argument of the |\*tref*| macros. To specify the |cdbase|, we have to
-% resort to the |\termref| macro with the keyval arguments.
-%
-% Note that the |\termref| treatment above is natural for ``concepts'' declared by the
-% |\termdef| macro from the |modules| package~\ctancite{KohAmb:smmssl}. Concepts are
-% natural language names for mathematical objects. For ``symbols'', i.e. symbolic
-% identifiers for mathematical objects used in mathematical formulae, we use the |\symdef|
-% macro from the |modules| package. Sometimes, symbols also have an associated natural
-% language concept, and we want to use the symbol name to reference it (instead of
-% specifying |cd| and |name| which is more inconvenient). For this the |statements|
-% package supplies the \DescribeMacro{\symref}|\symref| macro. Like |\termref|, and
-% invocation of |\symref{|\meta{cseq}|}{|\meta{text}|}| will just typeset \meta{text} with
-% a hyperlink to the relevant definition (i.e. the one that has the declaration
-% |for=|\meta{cseq} in the metadata argument.)
-%
-% The \DescribeMacro{\term}|\term| macro is a variant of the |\termref| macro that marks
-% up a phrase as a (possible) term reference, which does not have a link \emph{yet}. This
-% macro is a convenient placeholder for authoring, where a |\termref| annotation is
-% (currently) too tedious or the link target has not been authored yet. It facilitates
-% lazy flexiformalization workflows, where definitions for mathematical concepts are
-% supplied or marked up by need (e.g. after a |grep| shows that the number of |\term|
-% annotations of a concept is above a threshold). Editors or active documents can also
-% support the |\term| macro like a wiki-like dangling link: a click on
-% |\term{|\meta{phrase}|}| could generate a new editor buffer with a stub definition (an
-% |definition| environment with |\definiendum| macro and appropriate metadata).\ednote{MK:
-% we probably need multi-part variants for |?tref*|}
-%
-% \section{Configuration of the Presentation}\label{sec:conf}
-%
-% \DescribeMacro{\defemph} The |\defemph| macro is a configuration hook that allows to
-% specify the style of presentation of the {\index*{definiendum}}. By default, it is set to
-% |\bf| as a fallback, since we can be sure that this is always available. It can be
-% customized by redefinition: For instance |\renewcommand{\defemph}[1]{\emph{#1}}|,
-% changes the default behavior to italics.
-%
-% \DescribeMacro{\termemph} The |\termenph| macro does the same for the style for
-% |\termref|, it is empty by default. Note the term might carry an implicit hyper-reference
-% to the defining occurrence and that the presentation engine might mark this up, changing
-% this behavior.
-%
-% \DescribeMacro{\stDMemph} The |\stDMemph| macro does the same for the style for the
-% markup of the discourse markers like ``Theorem''. If it is not defined, it is set to
-% |\bf|; that allows to preset this in the class file. \ednote{function declarations}
-%
-% Some authors like to lowercase the semantic references, i.e. use ``axiom 2.6'' instead
-% of the default ``\sref{peano.P5}'' to refer to the last axiom in
-% Figure~\ref{fig:axioms}. This can be achieved by redefining the
-% \DescribeMacro{\STpresent}|\STpresent| macro, which is applied to the keyword of the
-% |ST*Env| theorem environments.\ednote{this does not quite work as yet, since
-% \textbf{STpresent} is applied when the label is written. But we would really like to
-% have it applied when the reference is constructed. But for that we need to split the
-% label into keyword and number in package |sref|.}
-%
-% Finally, we provide configuration hooks in Figure~\ref{fig:hooks} for the statement
-% types provided by the |statement| package. These are mainly intended for package
-% authors building on |statements|, e.g. for multi-language support. The language
-% bindings are given in the |smultiling|~\cite{KohGin:smss:svn} package not in
-% |statements| itself.
-%
-%\begin{exfig}
-% \begin{tabular}{lll}
-% Environment & configuration macro & value\\\hline\hline
-% \texttt{STtheoremAssEnv} & \texttt{\textbackslash st@theorem@kw} & \makeatletter\st@theorem@kw\\\hline
-% \texttt{STlemmaAssEnv} & \texttt{\textbackslash st@lemma@kw} & \makeatletter\st@lemma@kw \\\hline
-% \texttt{STpropositionAssEnv} & \texttt{\textbackslash st@proposition@kw} & \makeatletter\st@proposition@kw \\\hline
-% \texttt{STcorollaryAssEnv} & \texttt{\textbackslash st@corollary@kw} & \makeatletter\st@corollary@kw\\\hline
-% \texttt{STconjectureAssEnv} & \texttt{\textbackslash st@conjecture@kw} & \makeatletter\st@conjecture@kw\\\hline
-% \texttt{STfalseconjectureAssEnv} & \texttt{\textbackslash st@falseconjecture@kw} & \makeatletter\st@falseconjecture@kw\\\hline
-% \texttt{STpostulateAssEnv} & \texttt{\textbackslash st@postulate@kw} & \makeatletter\st@postulate@kw\\\hline
-% \texttt{STobligationAssEnv} & \texttt{\textbackslash st@obligation@kw} & \makeatletter\st@obligation@kw\\\hline
-% \texttt{STassumptionAssEnv} & \texttt{\textbackslash st@assumption@kw} & \makeatletter\st@assumption@kw\\\hline
-% \texttt{STobservationAssEnv} & \texttt{\textbackslash st@observation@kw} & \makeatletter\st@observation@kw\\\hline
-% \texttt{STremarkAssEnv} & \texttt{\textbackslash st@remark@kw} & \makeatletter\st@remark@kw\\\hline
-% \texttt{STruleAssEnv} & \texttt{\textbackslash st@rule@kw} & \makeatletter\st@rule@kw\\\hline
-% \texttt{STexampleEnv} & \texttt{\textbackslash st@example@kw} & \makeatletter\st@example@kw\\\hline
-% \texttt{STaxiomEnv} & \texttt{\textbackslash st@axiom@kw} & \makeatletter\st@axiom@kw\\\hline
-% \texttt{STdefinitionEnv} & \texttt{\textbackslash st@definition@kw} & \makeatletter\st@definition@kw\\\hline
-% \texttt{STnotationEnv} & \texttt{\textbackslash st@notation@kw} & \makeatletter\st@notation@kw
-% \end{tabular}
-% \caption{Configuration Hooks for statement types}\label{fig:hooks}
-% \end{exfig}
-%
-% \section{Limitations}\label{sec:limitations}
-%
-% In this section we document known limitations. If you want to help alleviate them,
-% please feel free to contact the package author. Some of them are currently discussed in
-% the \sTeX GitHub repository~\cite{sTeX:github:on}.
-% \begin{enumerate}
-% \item none reported yet
-% \end{enumerate}
-%
-% \StopEventually{\newpage\PrintIndex\newpage\PrintChanges\printbibliography}
-%
-% \section{The Implementation}\label{sec:impl}
-%
-% \subsection{Package Options}\label{sec:impl:options}
-%
-% We declare some switches which will modify the behavior according to the package
-% options. Generally, an option |xxx| will just set the appropriate switches to true
-% (otherwise they stay false). First we have the general options: |msection| specifies
-% that theorems should be numbered in the |msection| counter provided by the |mikoslides|
-% package/class.
-% \begin{macrocode}
-%<*package>
-\newif\ifdef@index\def@indexfalse
-\DeclareOption{defindex}{\def@indextrue}
-\newif\if@nthm\@nthmtrue
-\DeclareOption{nontheorem}{\@nthmfalse}
-\newif\if@msection\@msectionfalse
-\DeclareOption{msection}{\@msectiontrue}
-\DeclareOption*{\PassOptionsToPackage{\CurrentOption}{omtext}}
-\ProcessOptions
-% \end{macrocode}
-%
-% The next measure is to ensure that some {\sTeX} packages are loaded: |omdoc| for the
-% statement keys, |modules| since we need module identifiers for referencing. Furthermore,
-% we need the |ntheorem| package for presenting statements.
-% \begin{macrocode}
-\RequirePackage{omtext}
-\RequirePackage[base]{babel}
-\ifcsdef{proof}{\cslet{proof}{\relax}\cslet{endproof}{\relax}}{}% to redefine if necessary
-\if@nthm
-\RequirePackage[hyperref]{ntheorem}
-\theoremstyle{plain}
-\else
-\RequirePackage{amsthm}
-\fi
-% \end{macrocode}
-% Now, we define an auxiliary function that lowercases strings
-% \begin{macrocode}
-% \end{macrocode}
-% Sometimes it is necessary to fallback to symbol names in order to generate xml:id
-% attributes. For this purpose, we define an auxiliary function which ensures the name
-% receives a unique NCName equivalent.\ednote{Hard to be unique here, e.g. the names
-% "foo\_bar" and "foo bar" would receive the same xml:id attributes... of course we can
-% devise a more complex scheme for the symbol replacement.}
-% \begin{macrocode}
-% \end{macrocode}
-% The following functions are strictly utility functions that makes our life easier later on
-% \begin{macrocode}
-% \end{macrocode}
-%
-% For the other languages, we set up triggers
-% \begin{macrocode}
-\AfterBabelLanguage{ngerman}{\input{statements-ngerman.ldf}}
-\AfterBabelLanguage{arabic}{\input{statements-arabic.ldf}}
-% \end{macrocode}
-%
-% \subsection{Statements}\label{sec:impl:statements}
-%
-% \begin{macro}{\STpresent}
-% \begin{macrocode}
-\providecommand\STpresent[1]{#1}
-% \end{macrocode}
-% \end{macro}
-%
-% \begin{macro}{\define@statement@env}
-% We define a meta-macro that allows us to define several variants of statements. Upon
-% beginning this environment, we first set the |KeyVal| attributes, then we decide
-% whether to print the discourse marker based on the value of the |display| key, then
-% (given the right Options were set), we show the semantic annotations, and finally
-% initialize the environment using the appropriate macro. Upon ending the environment,
-% we just run the respective termination macro.
-% \begin{macrocode}
-\def\define@statement@env#1{%
-\ifcsdef{#1}{\cslet{#1}{\relax}\cslet{end#1}{\relax}}{}% to redefine if necessary
-\newenvironment{#1}[1][]{\metasetkeys{omtext}{##1}\sref@target%
-\@in@omtexttrue%
-\ifx\omtext@display\st@flow\else%
-\ifx\omtext@title\@empty\begin{ST#1Env}\else\begin{ST#1Env}[\omtext@title]\fi%
-\ifx\sref@id\@empty\else\label{#1.\sref@id}\fi
-\csname st@#1@initialize\endcsname\fi% display
-\ifx\sref@id\@empty\sref@label@id{here}\else%
-\sref@label@id{\STpresent{\csname st@#1@kw\endcsname}~\@currentlabel}\fi%
-\strut\ignorespaces}
-{\csname st@#1@terminate\endcsname\ifx\omtext@display\st@flow\else\end{ST#1Env}\fi%
-\omtext@post@skip\@in@omtextfalse}}
-% \end{macrocode}
-% \end{macro}
-%
-% \begin{environment}{assertion}
-% \begin{macrocode}
-\newenvironment{assertion}[1][]{\metasetkeys{omtext}{#1}\sref@target%
-\@in@omtexttrue%
-\ifx\omtext@display\st@flow
- \itshape\noindent\ignorespaces%
-\else% display!=flow
- \xdef\@@@type{\omtext@type}% to keep it safe from \inlinedef
- \ifx\omtext@title\@empty\begin{ST\@@@type AssEnv}%
- \else\begin{ST\@@@type AssEnv}[\omtext@title]%
- \fi%
-\fi %display=flow
-\ifx\omtext@type\@empty\else%
-\sref@label@id{\STpresent{\csname st@\@@@type @kw\endcsname}~\@currentlabel}
-\fi}
-{\ifx\omtext@display\st@flow\else\end{ST\@@@type AssEnv}\@in@omtextfalse\fi}
-% \end{macrocode}
-% \end{environment}
-%
-% \begin{macro}{\st@*@kw}
-% We configure the default keywords for the various theorem environments.
-% \begin{macrocode}
-\def\st@theorem@kw{Theorem}
-\def\st@lemma@kw{Lemma}
-\def\st@proposition@kw{Proposition}
-\def\st@corollary@kw{Corollary}
-\def\st@conjecture@kw{Conjecture}
-\def\st@falseconjecture@kw{Conjecture (false)}
-\def\st@postulate@kw{Postulate}
-\def\st@obligation@kw{Obligation}
-\def\st@assumption@kw{Assumption}
-\def\st@rule@kw{Rule}
-\def\st@observation@kw{Observation}
-\def\st@remark@kw{Remark}
-% \end{macrocode}
-%
-% \end{macro}
-% Then we configure the presentation of the theorem environments
-% \begin{macrocode}
-\if@nthm
-\theorembodyfont{\itshape}
-\theoremheaderfont{\normalfont\bfseries}
-\else
-\theoremstyle{plain}
-\fi
-% \end{macrocode}
-%
-% \begin{environment}{ST*AssEnv}
-% We define a number of internal assertion environments according to the values of its
-% |type| key.
-% \begin{macrocode}
-\if@msection
-\newtheorem{STtheoremAssEnv}{\st@theorem@kw}[msection]
-\else
-\ifdef{\thesection}
-{\newtheorem{STtheoremAssEnv}{\st@theorem@kw}[section]}
-{\newtheorem{STtheoremAssEnv}{\st@theorem@kw}}
-\fi
-\newtheorem{STlemmaAssEnv}[STtheoremAssEnv]{\st@lemma@kw}
-\newtheorem{STpropositionAssEnv}[STtheoremAssEnv]{\st@proposition@kw}
-\newtheorem{STcorollaryAssEnv}[STtheoremAssEnv]{\st@corollary@kw}
-\newtheorem{STconjectureAssEnv}[STtheoremAssEnv]{\st@conjecture@kw}
-\newtheorem{STfalseconjectureAssEnv}[STtheoremAssEnv]{\st@falseconjecture@kw}
-\newtheorem{STpostulateAssEnv}[STtheoremAssEnv]{\st@postulate@kw}
-\newtheorem{STobligationAssEnv}[STtheoremAssEnv]{\st@obligation@kw}
-\newtheorem{STassumptionAssEnv}[STtheoremAssEnv]{\st@assumption@kw}
-\newtheorem{STobservationAssEnv}[STtheoremAssEnv]{\st@observation@kw}
-\if@nthm\theorembodyfont{\rmfamily}\else\theoremstyle{definition}\fi
-\newtheorem{STremarkAssEnv}[STtheoremAssEnv]{\st@remark@kw}
-\newtheorem{STruleAssEnv}[STtheoremAssEnv]{\st@rule@kw}
-% \end{macrocode}
-% \end{environment}
-%
-% \begin{environment}{example}
-% \begin{macrocode}
-\def\st@example@initialize{}\def\st@example@terminate{}
-\define@statement@env{example}
-\def\st@example@kw{Example}
-\newtheorem{STexampleEnv}[STtheoremAssEnv]{\st@example@kw}
-% \end{macrocode}
-% \end{environment}
-%
-% \begin{environment}{axiom}
-% \begin{macrocode}
-\def\st@axiom@initialize{}\def\st@axiom@terminate{}
-\define@statement@env{axiom}
-\def\st@axiom@kw{Axiom}
-\newtheorem{STaxiomEnv}[STtheoremAssEnv]{\st@axiom@kw}
-% \end{macrocode}
-% \end{environment}
-%
-% \begin{environment}{symboldec}
-% We use |\symdef@type| from the |modules| package as the visual cue.
-% \begin{macrocode}
-\srefaddidkey{symboldec}
-\addmetakey{symboldec}{functions}
-\addmetakey{symboldec}{role}
-\addmetakey*{symboldec}{title}
-\addmetakey*{symboldec}{name}
-\addmetakey{symboldec}{subject}
-\addmetakey*{symboldec}{display}
-\newenvironment{symboldec}[1][]{\metasetkeys{symboldec}{#1}\sref@target\st@indeftrue%
-\ifx\symboldec@display\st@flow\else{\noindent\stDMemph{\symdef@type} \symboldec@name:}\fi%
-\ifx\symboldec@title\@empty~\else~(\stDMemph{\symboldec@title})\par\fi}{}
-% \end{macrocode}
-% \end{environment}
-%
-% \subsubsection{Types}\label{sec:impl:types}
-%
-% \begin{macro}{\symtype}\ednote{MK@DG; the type element should percolate up.}
-% \begin{macrocode}
-\srefaddidkey{symtype}
-\addmetakey*{symtype}{system}
-\addmetakey*{symtype}{for}
-\newcommand\type@type{Type}
-\newcommand\symtype[3][]{\metasetkeys{symtype}{#1}\sref@target%
-\noindent\type@type \ifx\symtype@\@empty\else (\symtype@system)\fi #2: $#3$}
-% \end{macrocode}
-% \end{macro}
-%
-% \begin{macro}{\inlinetypedec}
-% \begin{macrocode}
-\newcommand\inlinetypedec[3][]{\metasetkeys{symtype}{#1}\sref@target{\def\thedectype{#2}#3}}
-% \end{macrocode}
-% \end{macro}
-%
-% \begin{environment}{typedec}
-% We first define a theorem environment
-% \begin{macrocode}
-\def\st@typedec@kw{Type Declaration}
-\newtheorem{STtypedecEnv}[STtheoremAssEnv]{\st@typedec@kw}
-% \end{macrocode}
-% and then the environment itself.
-% \begin{macrocode}
-\newenvironment{typedec}[2][]{\metasetkeys{omtext}{#1}\sref@target%
-\def\thedectype{#2}%
-\ifx\omtext@display\st@flow\else%
-\ifx\omtext@title\@empty\begin{STtypedecEnv}\else\begin{STtypedecEnv}[\omtext@title]\fi%
-\ifx\sref@id\@empty\else\label{typedec.\sref@id}\fi
-\ifx\sref@id\@empty\sref@label@id{here}\else%
-\sref@label@id{\STpresent{\csname st@typedec@kw\endcsname}~\@currentlabel}\fi%
-\ignorespaces}
-{\ifx\omtext@display\st@flow\else\end{STtypedecEnv}\fi\omtext@post@skip}
-% \end{macrocode}
-% \end{environment}
-%
-% \begin{environment}{definition}
-% The |definition| environment itself is quite similar to the other's but we need to set
-% the |\st@indef| switch to suppress warnings from |\st@def@target|.
-% \begin{macrocode}
-\newif\ifst@indef\st@indeffalse
-\ifcsdef{definition}{\cslet{definition}{\relax}\cslet{enddefinition}{\relax}}{}% to redefine if necessary
-\newenvironment{definition}[1][]{\metasetkeys{omtext}{#1}\sref@target\st@indeftrue%
-\ifx\omtext@display\st@flow\else%
-\ifx\omtext@title\@empty\begin{STdefinitionEnv}\else\begin{STdefinitionEnv}[\omtext@title]\fi\fi%
-\ifx\sref@id\@empty\sref@label@id{here}\else%
-\sref@label@id{\STpresent{\csname st@definition@kw\endcsname}~\@currentlabel}\fi%
-\ignorespaces}
-{\ifx\omtext@display\st@flow\else\end{STdefinitionEnv}\fi}
-\def\st@definition@kw{Definition}
-\newtheorem{STdefinitionEnv}[STtheoremAssEnv]{\st@definition@kw}
-% \end{macrocode}
-% \end{environment}
-%
-% \begin{environment}{notation}
-% We initialize the |\def\st@notation@initialize{}| here, and extend it with
-% functionality below.
-% \begin{macrocode}
-\def\notemph#1{#1}
-\def\st@notation@terminate{}
-\def\st@notation@initialize{}
-\define@statement@env{notation}
-\def\st@notation@kw{Notation}
-\newtheorem{STnotationEnv}[STtheoremAssEnv]{\st@notation@kw}
-% \end{macrocode}
-% \end{environment}
-%
-% \begin{macro}{\st@def@target}
-% the next macro is a variant of the |\sref@target| macro provided by the |sref| package
-% specialized for the use in the |\definiendum|, |\defi*|, |\Defi*|, |\defi*s|, and |\Defi*s|
-% macros. |\st@def@target{|\meta{opt}|}{|\meta{name}|}{|\meta{text}|}| makes a target
-% with label |sref@|\meta{opt}|@|\meta{modulename}|@target|, if \meta{opt} is non-empty,
-% else with the label |sref@|\meta{name}|@|\meta{modulename}|@target| (the first time it
-% encounters this symbol; i.e. if |\sref@|\meta{name}|@|\meta{modulename}|@defined| is
-% undefined). And it formats the |\defemph|-emphasized \meta{text}. Also it generates
-% the necessary warnings for a definiendum-like macro.
-% \begin{macrocode}
-\newcommand\st@def@target[3]{\edef\@symname{#1}\def\@verbname{#2}%
-\ifst@indef% if we are in a definition or such
-\@ifundefined{mod@id}% if we are not in a module
-{\PackageWarning{statements}{definiendum in unidentified module\MessageBreak
-\protect\definiendum, \protect\defi*,
-\protect\Defi*, \protect\defi*s, \protect\Defi*s\MessageBreak
-can only be referenced when called in a module with id key}}%
-{% now we are in a module
-\edef\@@cd{\ifx\omtext@theory\@empty\mod@id\else\omtext@theory\fi}%
-\edef\@@name{\ifx\@symname\@empty\@verbname\else\@symname\fi}%
-\defemph{\@ifundefined{sref@\@@name @\@@cd @defined}%
-{\expandafter\sref@target@ifh{sref@\@@name @\@@cd @target}{#3}}%
-{#3}}%
-%\footnote{sTeX: target sref@\@@name @\@@cd @target}% for testing targets
-\expandafter\gdef\csname sref@\@@name @\@@cd @defined\endcsname{yes}%
-\ifmetakeys@showmeta\metakeys@show@keys{\@@cd}{name:\@@name}\fi}%
-\else% st@indef: we are not in a definition or such
-\PackageError{statements}%
-{definiendum outside definition context\MessageBreak
-\protect\definiendum, \protect\defi,
-\protect\Defi, \protect\defi*s, \protect\Defi*s\MessageBreak
-do not make sense semantically outside a definition.}
-{Consider wrapping the defining phrase in a \protect\inlinedef}%
-\fi}% st@indef
-% \end{macrocode}
-% \end{macro}
-%
-% The |\definiendum| and |\notatiendum| macros are very simple.
-%
-% \begin{macro}{\@termdef}
-% This macro is experimental, it is supposed to be invoked in |\definiendum| to define a
-% macro with the definiendum text, so that can be re-used later in term assignments (see
-% the |modules| package). But in the current context, where we rely on {\TeX} groupings
-% for visibility, this does not work, since the invocations of |\definiendum| are in
-% |definition| environments and thus one group level too low. Keeping this for future
-% reference.
-% \begin{macrocode}
-\newcommand\@termdef[2][]{\def\@test{#1}%
-\@ifundefined{mod@id}{}{\ifx\@test\@empty\def\@@name{#2}\else\def\@@name{#1}\fi%
-\termdef{\mod@id @\@@name}{#2}}}
-% \end{macrocode}
-% \end{macro}
-%
-% \begin{macro}{\definiendum}
-% \begin{macrocode}
-\addmetakey{definiendum}{name}
-\addmetakey{definiendum}{lemma}
-\newcommand\definiendum[2][]{\setkeys{definiendum}{#1}%
-\st@def@target{\definiendum@name}{\definiendum@name}{#2}}
-% \end{macrocode}
-% \end{macro}
-%
-% \begin{macro}{\notatiendum}
-% the |notatiendum| macro also needs to be visible in the |notation| and |definition|
-% environments
-% \begin{macrocode}
-\newcommand\notatiendum[2][]{\notemph{#2}}
-% \end{macrocode}
-% \end{macro}
-%
-% We expand the {\latexml} bindings for |\defi|, |\defii|, |\defiii| and |\defiv| into two
-% instances one will be used for the definition and the other for indexing.
-%
-% \begin{macro}{\defi}
-% We split the |\defi| macro in two: |\defi| does the definiendum bit and |\@defi|
-% handles the last optional argument and does the indexing. The information flow between
-% them goes via the local |\@phrase| macro.
-% \begin{macrocode}
-\newcommand\@defi[1][]{\ifdef@index\omdoc@indexi[#1]{\@phrase}\fi\xspace}
-\newcommand\defi[2][]{\metasetkeys{definiendum}{#1}%
-\st@def@target{\definiendum@name}{#2}{#2}\def\@phrase{#2}\@defi}
-\newcommand\defis[2][]{\metasetkeys{definiendum}{#1}%
-\st@def@target{\definiendum@name}{#2}{#2s}\def\@phrase{#2}\@defi}
-\newcommand\Defi[2][]{\metasetkeys{definiendum}{#1}%
-\st@def@target{\definiendum@name}{#2}{\capitalize{#2}}\def\@phrase{#2}\@defi}
-\newcommand\Defis[2][]{\metasetkeys{definiendum}{#1}%
-\st@def@target{\definiendum@name}{#2}{\capitalize{#2s}}\def\@phrase{#2}\@defi}
-% \end{macrocode}
-% \end{macro}
-%
-% \begin{macro}{\adefi}
-% Again we split the |\adefi| macro into two parts: |\adef| does the definiendum bit and
-% |\@adefi| handles the last optional argument and does the indexing.
-% \begin{macrocode}
-\newcommand\adefi[3][]{\metasetkeys{definiendum}{#1}\def\@verb{#3}%
-\st@def@target{\definiendum@name}{#3}{#2}\@adefi}
-\newcommand\@adefi[1][]{%
-\ifdef@index%
-\ifx\definiendum@name\@empty\omdoc@indexi[#1]{\@verb}%
-\else\omdoc@indexi[at=\definiendum@name,#1]{\@verb}\fi%
-\fi\xspace}
-% \end{macrocode}
-% \end{macro}
-%
-% \begin{macro}{\defii}
-% \begin{macrocode}
-\newcommand\@defii[1][]{\ifdef@index\omdoc@indexii[#1]{\@pone}{\@ptwo}\fi\xspace}
-\newcommand\defii[3][]{\metasetkeys{definiendum}{#1}%
-\def\@pone{#2}\def\@ptwo{#3}%
-\st@def@target{\definiendum@name}{#2-#3}{#2 #3}\@defii}
-\newcommand\defiis[3][]{\metasetkeys{definiendum}{#1}%
-\def\@pone{#2}\def\@ptwo{#3}%
-\st@def@target{\definiendum@name}{#2-#3}{#2 #3s}\@defii}
-\newcommand\Defii[3][]{\metasetkeys{definiendum}{#1}%
-\def\@pone{#2}\def\@ptwo{#3}%
-\st@def@target{\definiendum@name}{#2-#3}{\capitalize{#2 #3}}\@defii}
-\newcommand\Defiis[3][]{\metasetkeys{definiendum}{#1}%
-\def\@pone{#2}\def\@ptwo{#3}%
-\st@def@target{\definiendum@name}{#2-#3}{\capitalize{#2 #3s}}\@defii}
-% \end{macrocode}
-% \end{macro}
-%
-% \begin{macro}{\adefii}
-% analogous to |\adefi|
-% \begin{macrocode}
-\newcommand\adefii[4][]{\metasetkeys{definiendum}{#1}\def\@pone{#3}\def\@ptwo{#4}%
-\st@def@target{\definiendum@name}{#3-#4}{#2}\@adefii}
-\newcommand\@adefii[1][]{%
-\ifdef@index%
-\ifx\definiendum@name\@empty\omdoc@indexii[#1]{\@pone}{\@ptwo}%
-\else\omdoc@indexii[at=\definiendum@name,#1]{\@pone}{\@ptwo}\fi%
-\fi\xspace}
-% \end{macrocode}
-% \end{macro}
-%
-% \begin{macro}{\defiii}
-% similar to |\defii|
-% \begin{macrocode}
-\newcommand\@defiii[1][]{\ifdef@index\omdoc@indexiii[#1]{\@pone}{\@ptwo}{\@pthree}\fi\xspace}
-\newcommand\defiii[4][]{\metasetkeys{definiendum}{#1}%
-\def\@pone{#2}\def\@ptwo{#3}\def\@pthree{#4}%
-\st@def@target{\definiendum@name}{#2-#3-#4}{#2 #3 #4}\@defiii}
-\newcommand\defiiis[4][]{\metasetkeys{definiendum}{#1}%
-\def\@pone{#2}\def\@ptwo{#3}\def\@pthree{#4}%
-\st@def@target{\definiendum@name}{#2-#3-#4}{#2 #3 #4s}\@defiii}
-\newcommand\Defiii[4][]{\metasetkeys{definiendum}{#1}%
-\def\@pone{#2}\def\@ptwo{#3}\def\@pthree{#4}%
-\st@def@target{\definiendum@name}{#2-#3-#4}{\capitalize{#2 #3 #4}}\@defiii}
-\newcommand\Defiiis[4][]{\metasetkeys{definiendum}{#1}%
-\def\@pone{#2}\def\@ptwo{#3}\def\@pthree{#4}%
-\st@def@target{\definiendum@name}{#2-#3-#4}{\capitalize{#2 #3 #4s}}\@defiii}
-% \end{macrocode}
-% \end{macro}
-%
-% \begin{macro}{\adefiii}
-% \begin{macrocode}
-\newcommand\adefiii[5][]{\metasetkeys{definiendum}{#1}\def\@pone{#3}\def\@ptwo{#4}\def\@pthree{#5}%
-\st@def@target{\definiendum@name}{#3-#4-#5}{#2}\@adefiii}
-\newcommand\@adefiii[1][]{%
-\ifdef@index%
-\ifx\definiendum@name\@empty\omdoc@indexiii[#1]{\@pone}{\@ptwo}{\@pthree}%
-\else\omdoc@indexiii[at=\definiendum@name,#1]{\@pone}{\@ptwo}{\@pthree}\fi%
-\fi\xspace}
-% \end{macrocode}
-% \end{macro}
-%
-% \begin{macro}{\defiv}
-% similar to |\defiii|
-% \begin{macrocode}
-\newcommand\@defiv[1][]{\ifdef@index\omdoc@indexiv[#1]{\@pone}{\@ptwo}{\@pthree}{\@ptfour}\fi\xspace}
-\newcommand\defiv[5][]{\metasetkeys{definiendum}{#1}%
-\def\@pone{#2}\def\@ptwo{#3}\def\@pthree{#4}\def\@ptfour{#5}%
-\st@def@target{\definiendum@name}{#2-#3-#4-#5}{#2 #3 #4 #5}\@defiv}
-\newcommand\defivs[5][]{\metasetkeys{definiendum}{#1}%
-\def\@pone{#2}\def\@ptwo{#3}\def\@pthree{#4}\def\@ptfour{#5}%
-\st@def@target{\definiendum@name}{#2-#3-#4-#5}{#2 #3 #4 #5s}\@defiv}
-\newcommand\Defiv[5][]{\metasetkeys{definiendum}{#1}%
-\def\@pone{#2}\def\@ptwo{#3}\def\@pthree{#4}\def\@ptfour{#5}%
-\st@def@target{\definiendum@name}{#2-#3-#4-#5}{\capitalize{#2 #3 #4 #5}}\@defiv}
-\newcommand\Defivs[5][]{\metasetkeys{definiendum}{#1}%
-\def\@pone{#2}\def\@ptwo{#3}\def\@pthree{#4}\def\@ptfour{#5}%
-\st@def@target{\definiendum@name}{#2-#3-#4-#5}{\capitalize{#2 #3 #4 #5s}}\@defiv}
-% \end{macrocode}
-% \end{macro}
-%
-% \begin{macro}{\adefiv}
-% \begin{macrocode}
-\newcommand\adefiv[6][]{\metasetkeys{definiendum}{#1}%
-\def\@pone{#3}\def\@ptwo{#4}\def\@pthree{#5}\def\@ptfour{#6}%
-\st@def@target{\definiendum@name}{#3-#4-#5-#6}{#2}\@adefiv}
-\newcommand\@adefiv[1][]{%
-\ifdef@index%
-\ifx\definiendum@name\@empty\@indiv[#1]{\@pone}{\@ptwo}{\@pthree}{\@ptfour}%
-\else\@indiv[at=\definiendum@name,#1]{\@pone}{\@ptwo}{\@pthree}{\@ptfour}\fi%
-\fi\xspace}
-% \end{macrocode}
-% \end{macro}
-%
-% \begin{macro}{\inlineex}
-% \begin{macrocode}
-\newcommand\inlineex[2][]{\metasetkeys{omtext}{#1}%
-\sref@target\sref@label@id{here}#2}
-% \end{macrocode}
-% \end{macro}
-%
-% \begin{macro}{\inlineass}
-% \begin{macrocode}
-\newcommand\inlineass[2][]{\metasetkeys{omtext}{#1}%
-\sref@target\sref@label@id{here}#2}
-% \end{macrocode}
-% \end{macro}
-%
-% \begin{macro}{\inlinedef}
-% \begin{macrocode}
-\newcommand\inlinedef[2][]{\metasetkeys{omtext}{#1}%
-\if@in@omtext\else% we are not in an omtext or statement
-\PackageError{modules}{\protect\inlinedef\space outside a statement!}%
-{Try wrapping the paragraph in a\MessageBreak
-\protect\begin{omtext}, \protect\begin{assertion}, \protect\begin{axiom}, ... \MessageBreak
-whatever is suitable semantically}\fi%
-\sref@target\sref@label@id{here}\st@indeftrue #2}
-% \end{macrocode}
-% \end{macro}
-%
-% \subsection{Cross-Referencing Symbols and Concepts}\label{sec:impl:crossref}
-%
-% \begin{macro}{\termref}
-% |\termref{|\meta{opt}|}{|\meta{text}|}| makes a hyperlink with link text \meta{text}
-% to the definitional occurrence of the symbol specified by the |name|, |cd|, and
-% |cdbase| keys in \meta{opt}. We first set sensible defaults if the keys are not
-% given. If the symbol is defined in the current document (i.e. if the macro
-% |\sref@|\meta{name}|@|\meta{cd}|@defined| is defined), then we make a local hyperref,
-% otherwise we punt to |\mod@termref|.
-% \begin{macrocode}
-\addmetakey*{termref}{cd}
-\addmetakey*{termref}{cdbase}
-\addmetakey*{termref}{name}
-\addmetakey*{termref}{role}
-\newcommand\termref[2][]{\metasetkeys{termref}{#1}%
-\ifx\termref@cd\@empty\def\termref@cd{\mod@id}\fi%
-\ifx\termref@name\@empty\def\termref@name{#2}\fi%
-\@ifundefined{sref@\termref@name @\termref@cd @defined}%
-{\ifx\termref@cdbase\@empty% external reference
-\mod@termref\termref@cd\termref@name{#2}%
-\else\sref@href@ifh\termref@cdbase{#2}%
-\fi}%
-{\def\@label{sref@\termref@name @\termref@cd @target}%
-\sref@hlink@ifh\@label{#2}%\footnote{termref: internal reference to \@label}
-}}
-% \end{macrocode}
-% \end{macro}
-%
-% \begin{macro}{\tref*}
-% \begin{macrocode}
-\newcommand\atrefi[3][]{\def\@test{#1}%
-\ifx\@test\@empty\termref[name=#3]{#2}\else\termref[cd=#1,name=#3]{#2}\fi}
-\newcommand\atrefii[4][]{\atrefi[#1]{#2}{#3-#4}}
-\newcommand\atrefiii[5][]{\atrefi[#1]{#2}{#3-#4-#5}}
-\newcommand\atrefiv[6][]{\atrefi[#1]{#2}{#3-#4-#5-#6}}
-% \end{macrocode}
-% \end{macro}
-%
-% \begin{macro}{\tref*}
-% \begin{macrocode}
-\newcommand\trefi[2][]{\atrefi[#1]{#2}{#2}}
-\newcommand\trefii[3][]{\atrefi[#1]{#2 #3}{#2-#3}}
-\newcommand\trefiii[4][]{\atrefi[#1]{#2 #3 #4}{#2-#3-#4}}
-\newcommand\trefiv[5][]{\atrefi[#1]{#2 #3 #4 #5}{#2-#3-#4-#5}}
-\newcommand\trefis[2][]{\atrefi[#1]{#2s}{#2}}
-\newcommand\trefiis[3][]{\atrefi[#1]{#2 #3s}{#2-#3}}
-\newcommand\trefiiis[4][]{\atrefi[#1]{#2 #3 #4s}{#2-#3-#4}}
-\newcommand\trefivs[5][]{\atrefi[#1]{#2 #3 #4 #5s}{#2-#3-#4-#5}}
-% \end{macrocode}
-% \end{macro}
-%
-% \begin{macro}{\Tref*}
-% \begin{macrocode}
-\newcommand\Trefi[2][]{\atrefi[#1]{\capitalize{#2}}{#2}}
-\newcommand\Trefii[3][]{\atrefi[#1]{\capitalize{#2 #3}}{#2-#3}}
-\newcommand\Trefiii[4][]{\atrefi[#1]{\capitalize{#2 #3 #4}}{#2-#3-#4}}
-\newcommand\Trefiv[5][]{\atrefi[#1]{\capitalize{#2 #3 #4 #5}}{#2-#3-#4-#5}}
-\newcommand\Trefis[2][]{\atrefi[#1]{\capitalize{#2s}}{#2}}
-\newcommand\Trefiis[3][]{\atrefi[#1]{\capitalize{#2 #3s}}{#2-#3}}
-\newcommand\Trefiiis[4][]{\atrefi[#1]{\capitalize{#2 #3 #4s}}{#2-#3-#4}}
-\newcommand\Trefivs[5][]{\atrefi[#1]{\capitalize{#2 #3 #4 #5s}}{#2-#3-#4-#5}}
-% \end{macrocode}
-% \end{macro}
-%
-% Now we care about the configuration switches, they are set to sensible values, if they
-% are not defined already. These are just configuration parameters, which should not
-% appear in documents, therefore we do not provide {\latexml} bindings for them.
-% \begin{macro}{\*emph}
-% \begin{macrocode}
-\providecommand{\termemph}[1]{#1}
-\providecommand{\defemph}[1]{{\textbf{#1}}}
-\providecommand{\stDMemph}[1]{{\textbf{#1}}}
-% \end{macrocode}
-% \end{macro}
-%
-% \begin{macro}{\term}
-% The |\term| macro is used for wiki-style dangling links with editor support.\ednote{MK: document above}
-% \begin{macrocode}
-\newcommand\term[2][]{\def\@test{#1}%
-\ifx\@test\@empty\else
-\@ifundefined{module@defs@#1}{\PackageWarning{statements}%
-{{\protect\term} specifies module #1 which is not in
- scope\MessageBreak import it via e.g. via \protect\importmhmodule}}{}
-\fi%
-\PackageWarning{statements}%
-{Dangling link (\protect\term) for "#2" still needs to be specified}%
-\textcolor{blue}{\underline{#2}}}
-% \end{macrocode}
-% \end{macro}
-% \begin{macro}{\symref}
-% The |\symref| macros is quite simple, since we have done all the heavy lifting in the
-% |modules| package: we simply apply |\mod@symref@|\meta{arg1} to
-% \meta{arg2}.
-% \begin{macrocode}
-\newcommand\symref[2]{\@nameuse{mod@symref@#1}{#2}}
-% \end{macrocode}
-% \end{macro}
-%
-% \subsection{Deprecated Functionality}\label{sec:deprecated}
-%
-% In this section we centralize old interfaces that are only partially supported any
-% more.
-% \begin{macro}{\*def*}
-% \begin{macrocode}
-\newcommand\defin[2][]{\defi[#1]{#2}%
-\PackageWarning{statements}{\protect\defin\space is deprecated, use \protect\defi\space instead}}
-\newcommand\twindef[3][]{\defii[#1]{#2}{#3}%
-\PackageWarning{statements}{\protect\twindef\space is deprecated, use \protect\defii\space instead}}
-\newcommand\atwindef[4][]{\defiii[#1]{#2}{#3}{#4}%
-\PackageWarning{statements}{\protect\atwindef\space is deprecated, use \protect\defiii\space instead}}
-\newcommand\definalt[3][]{\adefi[#1]{#2}{#3}%
-\PackageWarning{statements}{\protect\definalt\space is deprecated, use \protect\adefi\space instead}}
-\newcommand\twindefalt[4][]{\adefii[#1]{#2}{#3}{#4}%
-\PackageWarning{statements}{\protect\twindefalt\space is deprecated, use \protect\adefii\space instead}}
-\newcommand\atwindefalt[5][]{\adefiii[#1]{#2}{#3}{#4}{#5}%
-\PackageWarning{statements}{\protect\atwindefalt\space is deprecated, use \protect\adefiii\space instead}}
-% \end{macrocode}
-% \end{macro}
-%
-% \begin{macro}{\*def*}
-% \begin{macrocode}
-\newcommand\twinref[3][]{\trefii[#1]{#2}{#3}%
-\PackageWarning{statements}{\protect\twinref\space is deprecated, use \protect\trefii\space instead}}
-\newcommand\atwinref[4][]{\atrefiii[#1]{#2}{#3}{#4}%
-\PackageWarning{statements}{\protect\atwindef\space is deprecated, use \protect\trefiii\space instead}}
-%</package>
-% \end{macrocode}
-% \end{macro}
-% \Finale
-%
-\endinput
-% \iffalse
-%%% Local Variables:
-%%% mode: doctex
-%%% TeX-master: t
-%%% End:
-% \fi
-% LocalWords: GPL structuresharing STR dtx keyval env envfalse idfalse idtrue typedec st
-% LocalWords: displayfalse envtrue displaytrue forfalse typefalse titlefalse filedate eg
-% LocalWords: continuesfalse fortrue fromtrue typetrue titletrue CPERL omdoc thedectype
-% LocalWords: continuestrue symboldec omtext RequirePackage lowcase lc ToString termin
-% LocalWords: foreach hyperref href hlink DefStatement OptionalKeyVals ne NeedsTeXFormat
-% LocalWords: KeyVal xml CMP simpleDef PatternDef DefStatement PatternRule thedectype
-% LocalWords: requation PatternCMP RecDef DefConstructor keyvals defs psymbols tref eset
-% LocalWords: openElement symb closeElement ffor getValue attrs metadata undef rangle
-% LocalWords: afterDigestBegin setProperty AssignValue afterDigest definiendum rangle
-% LocalWords: cd addr LookupValue getArg toString idx idt definiendum ide idp st@flow
-% LocalWords: DefMacro args unlist inlinedef uri pdf afterOpen numberIt texttt XMath
-% LocalWords: iffalse consymb ntheorem textbackslash symref def scsys sc sc kw endinput
-% LocalWords: mathml openmath latexml activemath fileversion maketitle stex importmodule
-% LocalWords: setcounter tocdepth tableofcontents newpage sproofs ulsmf08 sref usevocab
-% LocalWords: MaySch eltte09 twintoo sref subsubsection exfig vspace vspace usemhvocab
-% LocalWords: noindent renewtheorem hline textbf textbf footnotesize ple peano inlineass
-% LocalWords: STaxiomEnv symdef medskip succ mathbb ldots stepcounter ednote usemhmodule
-% LocalWords: STtheoremAssEnv stepcounter STtheoremAssEnv stepcounter defin STtypedecEnv
-% LocalWords: STtheoremAssEnv notatiendum defin smomdl biblatex twindef cdbase defis
-% LocalWords: twindef atwindef atwindef adjectivized varaiants twindefalt cseq defindex
-% LocalWords: twindefalt atwindefalt atwindefalt csymbol definalt termref emph emptyset
-% LocalWords: termref compactdesc KohAmb smmssl twinref atwinref newpart impl customized
-% LocalWords: termdef defemph defemph renewcommand termemph termenph stDMemph formalized
-% LocalWords: stDMemph STpresent STpresent makeatletter STlemmaAssEnv textsf emphasized
-% LocalWords: STpropositionAssEnv STcorollaryAssEnv STconjectureAssEnv langle defiis
-% LocalWords: STfalseconjectureAssEnv STpostulateAssEnv STobligationAssEnv foo defiis
-% LocalWords: STassumptionAssEnv STobservationAssEnv STexampleEnv textsf ltxml defiiis
-% LocalWords: STdefinitionEnv STnotationEnv printbibliography langle ncname localization
-% LocalWords: theoremstyle sym newenvironment ifx csname endcsname inlineex loadmodules
-% LocalWords: currentlabel theorembodyfont itshape theoremheaderfont bfseries defiiis
-% LocalWords: normalfont newtheorem upshape srefaddidkey definendum customization gdef
-% LocalWords: newcommand indef newif ifst indeffalse indeftrue attr whatsit automatized
-% LocalWords: STdefinitionEnvKeyword notemph modulename ifundefined atwin defi behavior
-% LocalWords: expandafter providecommand nameuse doctex ctancite funval defii initialize
-% LocalWords: funsymbs findnodes symbolnode defsref showmeta showmeta sysname ngerman
-% LocalWords: defii defiii defiii adefi adefi adefii adefii adefiii adefiii STruleAssEnv
-% LocalWords: trefi trefii trefiii atref atrefi atrefii atrefiii conf metakeys setkeys
-% LocalWords: compactenum Deref metasetkeys addmetakey symtype ltx ltx sts specialized
-% LocalWords: ifmetakeys fntype rightarrow inlinetypedec inlinetypedec STremarkAssEnv
-% LocalWords: ignorespaces usemodule textcolor STtypedecEnvKeyword flexiformalization
-% LocalWords: statements-ngerman.ldf omdoc@indexi xspace trefis trefiis trefiiis
-% LocalWords: importmhmodule
-
-% \endinput
-% Local Variables:
-% mode: doctex
-% TeX-master: t
-% End: