From 740a11f29a3551babe3d7edbb57ac3baa2280a3f Mon Sep 17 00:00:00 2001 From: Norbert Preining Date: Sat, 26 Feb 2022 03:00:34 +0000 Subject: CTAN sync 202202260300 --- .../contrib/stex/sty/statements/statements.dtx | 1304 -------------------- 1 file changed, 1304 deletions(-) delete mode 100644 macros/latex/contrib/stex/sty/statements/statements.dtx (limited to 'macros/latex/contrib/stex/sty/statements/statements.dtx') 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 -%\NeedsTeXFormat{LaTeX2e}[1999/12/01] -%\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} -% -% \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}} -% -% \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: -- cgit v1.2.3