summaryrefslogtreecommitdiff
path: root/macros/latex/contrib/stex/sty/sproof
diff options
context:
space:
mode:
Diffstat (limited to 'macros/latex/contrib/stex/sty/sproof')
-rw-r--r--macros/latex/contrib/stex/sty/sproof/README10
-rw-r--r--macros/latex/contrib/stex/sty/sproof/sproof.dtx775
-rw-r--r--macros/latex/contrib/stex/sty/sproof/sproof.ins30
-rw-r--r--macros/latex/contrib/stex/sty/sproof/sproof.pdfbin331925 -> 0 bytes
4 files changed, 0 insertions, 815 deletions
diff --git a/macros/latex/contrib/stex/sty/sproof/README b/macros/latex/contrib/stex/sty/sproof/README
deleted file mode 100644
index 6642685638..0000000000
--- a/macros/latex/contrib/stex/sty/sproof/README
+++ /dev/null
@@ -1,10 +0,0 @@
-sproof.sty: An Infrastructure for Structural Markup for Proofs
-
-This package supplies macros and environment that allow to annotate the structure of
-mathematical proofs. This structure can be used by MKM systems for added-value services,
-either directly from the sTeX sources, or after translation via the LaTeXML system.
-
-Copyright (c) 2008 Michael Kohlhase
-The package is distributed under the terms of the LaTeX Project Public License (LPPL)
-
-Project home: https://github.com/KWARC/sTeX/
diff --git a/macros/latex/contrib/stex/sty/sproof/sproof.dtx b/macros/latex/contrib/stex/sty/sproof/sproof.dtx
deleted file mode 100644
index 16f5226020..0000000000
--- a/macros/latex/contrib/stex/sty/sproof/sproof.dtx
+++ /dev/null
@@ -1,775 +0,0 @@
-% \iffalse meta-comment
-% An Infrastructure for Structural Markup for Proofs
-% Copyright (C) 2004-2011 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{sproof}[2019/03/20 v1.1 Semantic Markup for Proofs]
-%
-%<*driver>
-\documentclass{ltxdoc}
-\usepackage[utf8]{inputenc}
-\usepackage{url,array,stex,float,moreverb}
-\usepackage[show]{ed}
-\usepackage[hyperref=auto,style=alphabetic]{biblatex}
-\addbibresource{kwarcpubs.bib}
-\addbibresource{extpubs.bib}
-\addbibresource{kwarccrossrefs.bib}
-\addbibresource{extcrossrefs.bib}
-\usepackage{ctangit}
-\usepackage{paralist}
-\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{sproof.dtx}
-\end{document}
-%</driver>
-% \fi
-%
-% \CheckSum{341}
-%
-% \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}{2006/10/31}{made sproof.dtx independent of statements.dtx}
-% \changes{v0.9d}{2006/10/31}{revamped the proof end mark management}
-% \changes{v0.9e}{2008/10/11}{taking type seriously}
-% \changes{v0.9f}{2009/12/14}{changing to omd metadata framework}
-% \changes{v0.9f}{2008/12/14}{first steps to sref}
-% \changes{v1.0}{2011/01/23}{making proof step labels stylable}
-% \changes{v1.1}{2013/09/29}{subproof now more like proof (takes comment arg)}
-%
-% \GetFileInfo{sproof.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\cmathml{Content-{\sc MathML}\index{Content {\sc MathML}}\index{MathML@{\sc MathML}!content}}
-% \def\activemath{\scsys{ActiveMath}}
-% \def\twin#1#2{\index{#1!#2}\index{#2!#1}}
-% \def\twintoo#1#2{{#1 #2}\twin{#1}{#2}}
-% \def\atwin#1#2#3{\index{#1!#2!#3}\index{#3!#2 (#1)}}
-% \def\atwintoo#1#2#3{{#1 #2 #3}\atwin{#1}{#2}{#3}}
-% \title{{\texttt{sproof.sty}}: Structural Markup for Proofs\thanks{Version {\fileversion} (last revised
-% {\filedate})}}
-% \author{Michael Kohlhase\\
-% FAU Erlangen-N\"urnberg\\
-% \url{http://kwarc.info/kohlhase}}
-% \maketitle
-%
-% \begin{abstract}
-% The |sproof| 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 supplies macros and environment that allow to annotate the structure of
-% mathematical proofs 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}
-%
-% \newpage\tableofcontents\newpage
-%
-%\section{Introduction}\label{sec:sproof}
-%
-% The |sproof| ({\twintoo{semantic}{proofs}}) package supplies macros and environment that
-% allow to annotate the structure of mathematical proofs in {\stex} files. 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 |statements|.
-%
-% {\stex} 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).
-%
-% \begin{exfig}\scriptsize
-% \begin{verbatim}
-% \begin{sproof}[id=simple-proof,for=sum-over-odds]
-% {We prove that $\sum_{i=1}^n{2i-1}=n^{2}$ by induction over $n$}
-% \begin{spfcases}{For the induction we have to consider the following cases:}
-% \begin{spfcase}{$n=1$}
-% \begin{spfstep}[display=flow] then we compute $1=1^2$\end{spfstep}
-% \end{spfcase}
-% \begin{spfcase}{$n=2$}
-% \begin{sproofcomment}[display=flow]
-% This case is not really necessary, but we do it for the
-% fun of it (and to get more intuition).
-% \end{sproofcomment}
-% \begin{spfstep}[display=flow] We compute $1+3=2^{2}=4$.\end{spfstep}
-% \end{spfcase}
-% \begin{spfcase}{$n>1$}
-% \begin{spfstep}[type=assumption,id=ind-hyp]
-% Now, we assume that the assertion is true for a certain $k\geq 1$,
-% i.e. $\sum_{i=1}^k{(2i-1)}=k^{2}$.
-% \end{spfstep}
-% \begin{sproofcomment}
-% We have to show that we can derive the assertion for $n=k+1$ from
-% this assumption, i.e. $\sum_{i=1}^{k+1}{(2i-1)}=(k+1)^{2}$.
-% \end{sproofcomment}
-% \begin{spfstep}
-% We obtain $\sum_{i=1}^{k+1}{2i-1}=\sum_{i=1}^k{2i-1}+2(k+1)-1$
-% \begin{justification}[method=arith:split-sum]
-% by splitting the sum.
-% \end{justification}
-% \end{spfstep}
-% \begin{spfstep}
-% Thus we have $\sum_{i=1}^{k+1}{(2i-1)}=k^2+2k+1$
-% \begin{justification}[method=fertilize]
-% by inductive hypothesis.
-% \end{justification}
-% \end{spfstep}
-% \begin{spfstep}[type=conclusion]
-% We can \begin{justification}[method=simplify]simplify\end{justification}
-% the right-hand side to ${k+1}^2$, which proves the assertion.
-% \end{spfstep}
-% \end{spfcase}
-% \begin{spfstep}[type=conclusion]
-% We have considered all the cases, so we have proven the assertion.
-% \end{spfstep}
-% \end{spfcases}
-% \end{sproof}
-% \end{verbatim}
-% \vspace*{-.5cm}
-% \caption{A very explicit proof, marked up semantically}\label{fig:proof:src}
-% \end{exfig}
-%
-% We will go over the general intuition by way of our running example (see
-% Figure~\ref{fig:proof:src} for the source and Figure~\ref{fig:proof:result} for the
-% formatted result).\ednote{talk a bit more about proofs and their structure,... maybe
-% copy from OMDoc spec. }
-%
-% \section{The User Interface}
-%
-% \subsection{Package Options}\label{sec:user:options}
-%
-% The |sproof| package takes a single option: \DescribeMacro{showmeta}|showmeta|. If
-% this is set, then the metadata keys are shown (see~\cite{Kohlhase:metakeys:ctan} for details
-% and customization options).
-%
-% \subsection{Proofs and Proof steps}
-%
-% \DescribeEnv{sproof} The |proof| environment is the main container for proofs. It takes
-% an optional |KeyVal| argument that allows to specify the |id| (identifier) and |for|
-% (for which assertion is this a proof) keys. The regular argument of the |proof|
-% environment contains an introductory comment, that may be used to announce the proof
-% style. The |proof| environment contains a sequence of |\step|, |proofcomment|, and
-% |pfcases| environments that are used to markup the proof steps. The |proof| environment
-% has a variant |Proof|, which does not use the proof end marker. This is convenient, if a
-% proof ends in a case distinction, which brings it's own proof end marker with it.
-% \DescribeEnv{sProof} The |Proof| environment is a variant of |proof| that does not mark
-% the end of a proof with a little box; presumably, since one of the subproofs already has
-% one and then a box supplied by the outer proof would generate an otherwise empty line.
-% \DescribeMacro{\spfidea} The |\spfidea| macro allows to give a one-paragraph
-% description of the proof idea.
-%
-% For one-line proof sketches, we use the \DescribeMacro{spfsketch}|\spfsketch| macro,
-% which takes the |KeyVal| argument as |sproof| and another one: a natural language text
-% that sketches the proof.
-%
-% \DescribeEnv{spfstep} Regular proof steps are marked up with the |step| environment, which
-% takes an optional |KeyVal| argument for annotations. A proof step usually contains a
-% local assertion (the text of the step) together with some kind of evidence that this can
-% be derived from already established assertions.
-%
-% Note that both |\premise| and |\justarg| can be used with an empty second argument to
-% mark up premises and arguments that are not explicitly mentioned in the text.
-%
-% \begin{exfig}
-% \begin{sproof}[id=simple-proof,for=sum-over-odds]
-% {We prove that $\sum_{i=1}^n{2i-1}=n^{2}$ by induction over $n$}
-% \begin{spfcases}{For the induction we have to consider the following cases:}
-% \begin{spfcase}{$n=1$}
-% \begin{spfstep}[display=flow] then we compute $1=1^2$\end{spfstep}
-% \end{spfcase}
-% \begin{spfcase}{$n=2$}
-% \begin{sproofcomment}[display=flow]
-% This case is not really necessary, but we do it for the fun
-% of it (and to get more intuition).
-% \end{sproofcomment}
-% \begin{spfstep}[display=flow]
-% We compute $1+3=2^{2}=4$
-% \end{spfstep}
-% \end{spfcase}
-% \begin{spfcase}{$n>1$}
-% \begin{spfstep}[type=hypothesis,id=ind-hyp]
-% Now, we assume that the assertion is true for a certain $k\geq 1$, i.e.
-% $\sum_{i=1}^k{(2i-1)}=k^{2}$.
-% \end{spfstep}
-% \begin{sproofcomment}
-% We have to show that we can derive the assertion for $n=k+1$ from this
-% assumption, i.e. $\sum_{i=1}^{k+1}{(2i-1)}=(k+1)^{2}$.
-% \end{sproofcomment}
-% \begin{spfstep}[id=splitit]
-% We obtain $\sum_{i=1}^{k+1}{(2i-1)}=\sum_{i=1}^k{(2i-1)}+2(k+1)-1$
-% \begin{justification}[method=arith:split-sum]
-% by splitting the sum
-% \end{justification}
-% \end{spfstep}
-% \begin{spfstep}[id=byindhyp]
-% Thus we have $\sum_{i=1}^{k+1}{(2i-1)}=k^2+2k+1$
-% \begin{justification}[method=fertilize]
-% by \premise[ind-hyp]{inductive hypothesis}.
-% \end{justification}
-% \end{spfstep}
-% \begin{spfstep}[type=conclusion]
-% We can \begin{justification}[method=simplify-eq]
-% simplify the {\justarg[rhs]{right-hand side}}
-% \end{justification} to $(k+1)^2$, which proves the assertion.
-% \end{spfstep}
-% \end{spfcase}
-% \begin{spfstep}[type=conclusion]
-% We have considered all the cases, so we have proven the assertion.
-% \end{spfstep}
-% \end{spfcases}
-% \end{sproof}
-% \caption{The formatted result of the proof in Figure~\ref{fig:proof:src}}\label{fig:proof:result}
-% \end{exfig}
-%
-% \subsection{Justifications}
-%
-% \DescribeEnv{justification} This evidence is marked up with the |justification|
-% environment in the |sproof| package. This environment totally invisible to the formatted
-% result; it wraps the text in the proof step that corresponds to the evidence. The
-% environment takes an optional |KeyVal| argument, which can have the |method| key, whose
-% value is the name of a proof method (this will only need to mean something to the
-% application that consumes the semantic annotations). Furthermore, the justification can
-% contain ``premises'' (specifications to assertions that were used justify the step) and
-% ``arguments'' (other information taken into account by the proof method).
-%
-% \DescribeMacro{\premise} The |\premise| macro allows to mark up part of the text as
-% reference to an assertion that is used in the argumentation. In the example in
-% Figure~\ref{fig:proof:src} we have used the |\premise| macro to identify the inductive
-% hypothesis.
-%
-% \DescribeMacro{\justarg} The |\justarg| macro is very similar to |\premise| with the
-% difference that it is used to mark up arguments to the proof method. Therefore the
-% content of the first argument is interpreted as a mathematical object rather than as an
-% identifier as in the case of |\premise|. In our example, we specified that the
-% simplification should take place on the right hand side of the equation. Other examples
-% include proof methods that instantiate. Here we would indicate the substituted object in
-% a |\justarg| macro.
-%
-% \subsection{Proof Structure}
-%
-% \DescribeEnv{subproof} The |pfcases| environment is used to mark up a subproof. This
-% environment takes an optional |KeyVal| argument for semantic annotations and a second
-% argument that allows to specify an introductory comment (just like in the |proof|
-% environment). The \DescribeMacro{method}|method| key can be used to give the name of the
-% proof method executed to make this subproof.
-%
-% \DescribeEnv{spfcases} The |pfcases| environment is used to mark up a proof by
-% cases. Technically it is a variant of the |subproof| where the |method| is
-% |by-cases|. Its contents are |spfcase| environments that mark up the cases one by one.
-%
-% \DescribeEnv{spfcase} The content of a |pfcases| environment are a sequence of case
-% proofs marked up in the |pfcase| environment, which takes an optional |KeyVal| argument
-% for semantic annotations. The second argument is used to specify the the description of
-% the case under consideration. The content of a |pfcase| environment is the same as that
-% of a |proof|, i.e. |step|s, |proofcomment|s, and |pfcases|
-% environments. \DescribeMacro{\spfcasesketch}|\spfcasesketch| is a variant of the |spfcase|
-% environment that takes the same arguments, but instead of the |spfstep|s in the body
-% uses a third argument for a proof sketch.
-%
-% \DescribeEnv{sproofcomment} The |proofcomment| environment is much like a |step|, only
-% that it does not have an object-level assertion of its own. Rather than asserting some
-% fact that is relevant for the proof, it is used to explain where the proof is going,
-% what we are attempting to to, or what we have achieved so far. As such, it cannot be the
-% target of a |\premise|.
-%
-% \subsection{Proof End Markers}
-%
-% Traditionally, the end of a mathematical proof is marked with a little box at the end of
-% the last line of the proof (if there is space and on the end of the next line if there
-% isn't), like so:\sproofend
-%
-% The |sproof| package provides the \DescribeMacro{\sproofend}|\sproofend| macro for
-% this. If a different symbol for the proof end is to be used (e.g. {\sl{q.e.d}}), then
-% this can be obtained by specifying it using the
-% \DescribeMacro{\sProofEndSymbol}|\sProofEndSymbol| configuration macro (e.g. by specifying
-% |\sProofEndSymbol{q.e.d}|).
-%
-% Some of the proof structuring macros above will insert proof end symbols for sub-proofs,
-% in most cases, this is desirable to make the proof structure explicit, but sometimes
-% this wastes space (especially, if a proof ends in a case analysis which will supply its
-% own proof end marker). To suppress it locally, just set |proofend={}| in them or use use
-% |\sProofEndSymbol{}|.
-%
-% \subsection{Configuration of the Presentation}\label{sec:user:conf}
-%
-% Finally, we provide configuration hooks in Figure~\ref{fig:hooks} for the keywords in
-% proofs. These are mainly intended for package authors building on |statements|, e.g. for
-% multi-language support.\ednote{we might want to develop an extension
-% \texttt{sproof-babel} in the future.}.
-%\begin{figure}[ht]\centering
-% \begin{tabular}{|lll|}\hline
-% Environment & configuration macro & value\\\hline\hline
-% \texttt{sproof} & \texttt{\textbackslash spf@proof@kw} & \makeatletter\spf@proof@kw\\\hline
-% \texttt{sketchproof} & \texttt{\textbackslash spf@sketchproof@kw} & \makeatletter\spf@proofsketch@kw\\\hline
-% \end{tabular}
-% \caption{Configuration Hooks for Semantic Proof Markup}\label{fig:hooks}
-% \end{figure}
-% The proof step labels can be customized via the
-% \DescribeMacro{\pstlabelstyle}|\pstlabelstyle| macro: |\pstlabelstyle{|\meta{style}|}|
-% sets the style; see Figure~\ref{fig:pstlabel} for an overview of styles. Package writers
-% can add additional styles by adding a macro |\pst@make@label@|\meta{style} that takes
-% two arguments: a comma-separated list of ordinals that make up the prefix and the current
-% ordinal. Note that comma-separated lists can be conveniently iterated over by the
-% {\LaTeX} |\@for|\ldots|:=|\ldots|\do{|\ldots|}| macro; see Figure~\ref{fig:pstlabel} for
-% examples.
-%
-%\begin{figure}[ht]\centering\makeatletter\small
-% \begin{tabular}{|lll|}\hline
-% style & example& configuration macro\\\hline\hline
-% \texttt{long} & \pst@make@label@long{0,8,1}{5} & \verb|\def\pst@make@label@long#1#2{\@for\@I:=#1\do{\@I.}#2}|\\\hline
-% \texttt{angles} & \pst@make@label@angles{0,8,1}{5} & \verb|\def\pst@make@label@angles#1#2|\\
-% &&\quad\verb|{\ensuremath{\@for\@I:=#1\do{\rangle}}#2}|\\\hline
-% \texttt{short} & \pst@make@label@short{0,8,1}{5} & \verb|\def\pst@make@label@short#1#2{#2}|\\\hline
-% \texttt{empty} & \pst@make@label@empty{0,8,1}{5} & \verb|\def\pst@make@label@empty#1#2{}|\\\hline
-% \end{tabular}
-% \caption{Configuration Proof Step Label Styles}\label{fig:pstlabel}
-% \end{figure}
-%
-% \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 TRAC.
-% \begin{enumerate}
-% \item The numbering scheme of proofs cannot be changed. It is more geared for teaching
-% proof structures (the author's main use case) and not for writing papers.\lec{reported
-% by Tobias Pfeiffer (fixed)}
-% \item currently proof steps are formatted by the {\LaTeX} |description| environment. We
-% would like to configure this, e.g. to use the |inparaenum| environment for more
-% condensed proofs. I am just not sure what the best user interface would be I can
-% imagine redefining an internal environment |spf@proofstep@list| or adding a key
-% |prooflistenv| to the |proof| environment that allows to specify the environment
-% directly. Maybe we should do both.
-% \end{enumerate}
-%
-%
-% \StopEventually{\newpage\PrintIndex\newpage\PrintChanges\printbibliography}
-% \newpage
-%
-% \section{The Implementation}
-%
-% \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).\ednote{need an implementation for {\latexml}}
-%
-% \begin{macrocode}
-%<*package>
-\DeclareOption*{\PassOptionsToPackage{\CurrentOption}{sref}}
-\ProcessOptions
-% \end{macrocode}
-%
-% Then we make sure that the |sref| package is loaded~\ctancite{Kohlhase:sref}.
-% \begin{macrocode}
-\RequirePackage{sref}
-\RequirePackage{etoolbox}
-\RequirePackage[base]{babel}
-% \end{macrocode}
-%
-% \subsection{Proofs}\label{sec:impl:proofs}
-%
-% We first define some keys for the |proof| environment.
-% \begin{macrocode}
-\srefaddidkey{spf}
-\addmetakey*{spf}{display}
-\addmetakey{spf}{for}
-\addmetakey{spf}{from}
-\addmetakey*[\sproof@box]{spf}{proofend}
-\addmetakey{spf}{type}
-\addmetakey*{spf}{title}
-\addmetakey{spf}{continues}
-\addmetakey{spf}{functions}
-\addmetakey{spf}{method}
-% \end{macrocode}
-%
-% \begin{macro}{\spf@flow}
-% We define this macro, so that we can test whether the |display| key has the value |flow|
-% \begin{macrocode}
-\def\spf@flow{flow}
-% \end{macrocode}
-% \end{macro}
-%
-% For proofs, we will have to have deeply nested structures of enumerated list-like
-% environments. However, {\LaTeX} only allows |enumerate| environments up to nesting depth
-% 4 and general list environments up to listing depth 6. This is not enough for us.
-% Therefore we have decided to go along the route proposed by Leslie Lamport to use a
-% single top-level list with dotted sequences of numbers to identify the position in the
-% proof tree. Unfortunately, we could not use his |pf.sty| package directly, since it does
-% not do automatic numbering, and we have to add keyword arguments all over the place, to
-% accomodate semantic information.
-%
-% \begin{environment}{pst@with@label}
-% This environment manages\footnote{This gets the labeling right but only works 8 levels
-% deep} the path labeling of the proof steps in the description environment of the
-% outermost |proof| environment. The argument is the label prefix up to now; which we
-% cache in |\pst@label| (we need evaluate it first, since are in the right place
-% now!). Then we increment the proof depth which is stored in |\count10| (lower counters
-% are used by {\TeX} for page numbering) and initialize the next level counter
-% |\count\count10| with 1. In the end call for this environment, we just decrease the
-% proof depth counter by 1 again.
-% \begin{macrocode}
-\newenvironment{pst@with@label}[1]{%
- \edef\pst@label{#1}%
- \advance\count10 by 1%
- \count\count10=1%
-}{%
- \advance\count10 by -1%
-}%
-% \end{macrocode}
-% \end{environment}
-%
-% \begin{macro}{\the@pst@label}
-% |\the@pst@label| evaluates to the current step label.
-% \begin{macrocode}
-\def\the@pst@label{%
- \pst@make@label\pst@label{\number\count\count10}\pstlabel@postfix%
-}%
-% \end{macrocode}
-%\end{macro}
-%
-% \begin{macro}{\setpstlabelstyle}
-% |\setpstlabelstyle{|meta{Key-Val pairs}|}| makes the labeling style customizable.
-% |\setpstlabelstyle{prefix=Pr,delimiter=-,postfix=\dag}| will change the labeling style
-% from \textbf{P.1.2.3} to \textbf{Pr-1-2-3\dag}. |\setpstlabelstyledefault| will set the
-% labeling style back to default.
-% \begin{macrocode}
-\addmetakey[P]{pstlabel}{prefix}[]
-\addmetakey[.]{pstlabel}{delimiter}[]
-\addmetakey[]{pstlabel}{postfix}[]
-\metasetkeys{pstlabel}{}% initialization
-\newrobustcmd\setpstlabelstyle[1]{%
- \metasetkeys{pstlabel}{#1}%
-}%
-\newrobustcmd\setpstlabelstyledefault{%
- \metasetkeys{pstlabel}{prefix=P,delimiter=.,postfix=}%
-}%
-% \end{macrocode}
-%\end{macro}
-%
-% \begin{macro}{\pstlabelstyle}
-% |\pstlabelstyle| just sets the |\pst@make@label| macro according to the style.
-% \begin{macrocode}
-\def\pst@make@label@long#1#2{\@for\@I:=#1\do{\expandafter\@I\pstlabel@delimiter}#2}
-\def\pst@make@label@angles#1#2{\ensuremath{\@for\@I:=#1\do{\rangle}}#2}
-\def\pst@make@label@short#1#2{#2}
-\def\pst@make@label@empty#1#2{}
-\def\pstlabelstyle#1{%
- \def\pst@make@label{\@nameuse{pst@make@label@#1}}%
-}%
-\pstlabelstyle{long}%
-% \end{macrocode}
-%\end{macro}
-%
-% \begin{macro}{\next@pst@label}
-% |\next@pst@label| increments the step label at the current level.
-% \begin{macrocode}
-\def\next@pst@label{%
- \global\advance\count\count10 by 1%
-}%
-% \end{macrocode}
-%\end{macro}
-%
-%\begin{macro}{\sproofend}
-% This macro places a little box at the end of the line if there is space, or at the
-% end of the next line if there isn't
-% \begin{macrocode}
-\def\sproof@box{%
- \hbox{\vrule\vbox{\hrule width 6 pt\vskip 6pt\hrule}\vrule}%
-}%
-\def\spf@proofend{\sproof@box}%
-\def\sproofend{%
- \ifx\spf@proofend\@empty%
- \else%
- \hfil\null\nobreak\hfill\spf@proofend\par\smallskip%
- \fi%
-}%
-\def\sProofEndSymbol#1{\def\sproof@box{#1}}%
-% \end{macrocode}
-% \end{macro}
-%
-% \begin{macro}{spf@*@kw}
-% \begin{macrocode}
-\def\spf@proofsketch@kw{Proof Sketch}
-\def\spf@proof@kw{Proof}
-\def\spf@step@kw{Step}
-% \end{macrocode}
-% \end{macro}
-%
-% For the other languages, we set up triggers
-% \begin{macrocode}
-\AfterBabelLanguage{ngerman}{\input{sproof-ngerman.ldf}}
-\AfterBabelLanguage{arabic}{\input{sproof-arabic.ldf}}
-% \end{macrocode}
-%
-% \begin{macro}{spfsketch}
-% \begin{macrocode}
-\newrobustcmd\spfsketch[2][]{%
- \metasetkeys{spf}{#1}%
- \sref@target%
- \ifx\spf@display\spf@flow%
- \else%
- {\stDMemph{\ifx\spf@type\@empty\spf@proofsketch@kw\else\spf@type\fi}:}
- \fi{ #2}%
- \sref@label@id{this \ifx\spf@type\@empty\spf@proofsketch@kw\else\spf@type\fi}\sproofend%
-}%
-% \end{macrocode}
-% \end{macro}
-%
-% \begin{macro}{spfeq}
-% This is very similar to |\spfsketch|, but uses a computation array\ednote{This should
-% really be more like a tabular with an ensuremath in it. or invoke text on the last
-% column}\ednote{document above}
-% \begin{macrocode}
-\newenvironment{spfeq}[2][]{%
- \metasetkeys{spf}{#1}\sref@target%
- \ifx\spf@display\spf@flow%
- \else%
- {\stDMemph{\ifx\spf@type\@empty\spf@proof@kw\else\spf@type\fi}:} #2%
- \fi% display=flow
- \begin{displaymath}\begin{array}{rcll}%
-}{%
- \end{array}\end{displaymath}%
-}%
-% \end{macrocode}
-% \end{macro}
-%
-% \begin{environment}{sproof}
-% In this environment, we initialize the proof depth counter |\count10| to 10, and set
-% up the description environment that will take the proof steps. At the end of the
-% proof, we position the proof end into the last line.
-% \begin{macrocode}
-\newenvironment{spf@proof}[2][]{%
- \metasetkeys{spf}{#1}%
- \sref@target%
- \count10=10%
- \par\noindent%
- \ifx\spf@display\spf@flow%
- \else%
- \stDMemph{\ifx\spf@type\@empty\spf@proof@kw\else\spf@type\fi}:%
- \fi{ #2}%
- \sref@label@id{this \ifx\spf@type\@empty\spf@proof@kw\else\spf@type\fi}%
- \def\pst@label{}%
- \newcount\pst@count% initialize the labeling mechanism
- \begin{description}\begin{pst@with@label}{\pstlabel@prefix}%
-}{%
- \end{pst@with@label}\end{description}%
-}%
-\newenvironment{sproof}[2][]{\begin{spf@proof}[#1]{#2}}{\sproofend\end{spf@proof}}%
-\newenvironment{sProof}[2][]{\begin{spf@proof}[#1]{#2}}{\end{spf@proof}}%
-% \end{macrocode}
-% \end{environment}
-%
-% \begin{environment}{spfidea}
-% \begin{macrocode}
-\newrobustcmd\spfidea[2][]{%
- \metasetkeys{spf}{#1}%
- \stDMemph{\ifx\spf@type\@empty{Proof Idea}\else\spf@type\fi:} #2\sproofend%
-}%
-% \end{macrocode}
-% \end{environment}
-%
-% The next two environments (proof steps) and comments, are mostly semantical, they take
-% |KeyVal| arguments that specify their semantic role. In draft mode, they read these
-% values and show them. If the surrounding proof had |display=flow|, then no new |\item| is
-% generated, otherwise it is. In any case, the proof step number (at the current level) is
-% incremented.
-% \begin{environment}{spfstep}
-% \ednote{MK: labeling of steps does not work yet.}
-% \begin{macrocode}
-\newenvironment{spfstep}[1][]{%
- \metasetkeys{spf}{#1}%
- \@in@omtexttrue%
- \ifx\spf@display\spf@flow%
- \else%
- \item[\the@pst@label]%
- \fi%
- \ifx\spf@title\@empty\else{(\stDMemph{\spf@title}) }\fi%
- \sref@label@id{\pst@label}\ignorespaces%
-}{%
- \next@pst@label\@in@omtextfalse\ignorespaces%
-}%
-% \end{macrocode}
-% \end{environment}
-%
-% \begin{environment}{sproofcomment}
-% \begin{macrocode}
-\newenvironment{sproofcomment}[1][]{%
- \metasetkeys{spf}{#1}%
- \ifx\spf@display\spf@flow\else\item[\the@pst@label]\fi%
-}{%
- \next@pst@label%
-}%
-% \end{macrocode}
-% \end{environment}
-%
-% The next two environments also take a |KeyVal| argument, but also a regular one, which
-% contains a start text. Both environments start a new numbered proof level.
-%
-% \begin{environment}{subproof}
-% In the |subproof| environment, a new (lower-level) proproofof environment is started.
-% \begin{macrocode}
-\newenvironment{subproof}[2][]{%
- \metasetkeys{spf}{#1}%
- \def\@test{#2}%
- \ifx\@test\empty%
- \else%
- \ifx\spf@display\spf@flow {#2}%
- \else%
- \item[\the@pst@label]{#2} %
- \fi%
- \fi%
- \begin{pst@with@label}{\pst@label,\number\count\count10}%
-}{%
- \end{pst@with@label}\next@pst@label%
-}%
-% \end{macrocode}
-% \end{environment}
-%
-% \begin{environment}{spfcases}
-% In the |pfcases| environment, the start text is displayed as the first comment of the
-% proof.
-% \begin{macrocode}
-\newenvironment{spfcases}[2][]{%
- \def\@test{#1}%
- \ifx\@test\empty%
- \begin{subproof}[method=by-cases]{#2}%
- \else%
- \begin{subproof}[#1,method=by-cases]{#2}%
- \fi%
-}{%
- \end{subproof}%
-}%
-% \end{macrocode}
-% \end{environment}
-%
-% \begin{environment}{spfcase}
-% In the |pfcase| environment, the start text is displayed specification of the case
-% after the |\item|
-% \begin{macrocode}
-\newenvironment{spfcase}[2][]{%
- \metasetkeys{spf}{#1}%
- \ifx\spf@display\spf@flow\else\item[\the@pst@label]\fi%
- \def\@test{#2}%
- \ifx\@test\@empty%
- \else%
- {\stDMemph{#2}: }% need blank here
- \fi%
- \begin{pst@with@label}{\pst@label,\number\count\count10}
-}{%
- \ifx\spf@display\spf@flow%
- \else%
- \sproofend%
- \fi%
- \end{pst@with@label}%
- \next@pst@label%
-}%
-% \end{macrocode}
-% \end{environment}
-%
-% \begin{environment}{spfcase}
-% similar to |spfcase|, takes a third argument.
-% \begin{macrocode}
-\newrobustcmd\spfcasesketch[3][]{%
- \metasetkeys{spf}{#1}%
- \ifx\spf@display\spf@flow%
- \else%
- \item[\the@pst@label]%
- \fi%
- \def\@test{#2}%
- \ifx\@test\@empty%
- \else%
- {\stDMemph{#2}: }%
- \fi#3%
- \next@pst@label%
-}%
-% \end{macrocode}
-% \end{environment}
-%
-% \subsection{Justifications}
-%
-% We define the actions that are undertaken, when the keys for justifications are
-% encountered. Here this is very simple, we just define an internal macro with the value,
-% so that we can use it later.
-% \begin{macrocode}
-\srefaddidkey{just}
-\addmetakey{just}{method}
-\addmetakey{just}{premises}
-\addmetakey{just}{args}
-% \end{macrocode}
-%
-% The next three environments and macros are purely semantic, so we ignore the keyval
-% arguments for now and only display the content.\ednote{need to do something about the
-% premise in draft mode.}
-%
-% \begin{environment}{justification}
-% \begin{macrocode}
-\newenvironment{justification}[1][]{}{}
-% \end{macrocode}
-% \end{environment}
-%
-% \begin{macro}{\premise}
-% \begin{macrocode}
-\newrobustcmd\premise[2][]{#2}
-% \end{macrocode}
-% \end{macro}
-%
-% \begin{macro}{\justarg}
-% the |\justarg| macro is purely semantic, so we ignore the keyval arguments for now and
-% only display the content.
-% \begin{macrocode}
-\newrobustcmd\justarg[2][]{#2}
-%</package>
-% \end{macrocode}
-% \end{macro}
-%
-% \Finale
-\endinput
-%%% Local Variables:
-%%% mode: doctex
-%%% TeX-master: t
-%%% End:
-% LocalWords: GPL structuresharing STR sproof dtx CPERL keyval methodfalse env
-% LocalWords: methodtrue envtrue medhodtrue DefKeyVal Semiverbatim omdoc args
-% LocalWords: DefEnvironment OptionalKeyVals KeyVal omtext DefConstructor str
-% LocalWords: proofidea KeyVal pfstep DefCMPEnvironment KeyVal proofcomment eq
-% LocalWords: KeyVal pfcases KeyVal pfcase KeyVal extractBodyText unlist elsif
-% LocalWords: foreach getBody toString str str str LookupValue LastSeenCMP Thu
-% LocalWords: appendText getValue undef openElement closeElement DefMacro omd
-% LocalWords: afterClose nodeType childNodes firstCMP localname hasChildNodes
-% LocalWords: firstChild textContent removeChild iffalse kohlhase sref scsys
-% LocalWords: sproofs.sty sc sc mathml openmath latexml cmathml activemath geq
-% LocalWords: twintoo atwin atwintoo texttt fileversion maketitle stex newpage
-% LocalWords: tableofcontents newpage exfig scriptsize vspace ednote spfidea
-% LocalWords: spfidea spfsketch spfsketch spfstep justarg spfcases spfcase rhs
-% LocalWords: sproofcomment ind-hyp splitit arith byindhyp sproofend proofend
-% LocalWords: printbibliography textsf langle textsf langle ltxml ctancite spf
-% LocalWords: srefaddidkey pf.sty newenvironment hbox vrule vbox ifx showmeta
-% LocalWords: hrule vskip hrule vrule hfil nobreak hfill smallskip newcommand
-% LocalWords: stDMemph newcount endsproof xref doctex showmeta hline lec ldots
-% LocalWords: textbackslash makeatletter sketchproof compactenum tracissue
-% LocalWords: metakeys addmetakey metasetkeys stylable pstlabelstyle pstlabel
-% LocalWords: pstlabelstyle pstlabelstyle ldots ldots ensuremath inparaenum
-% LocalWords: nameuse prooflistenv spfcasesketch spfcasesketch spfeq rcll
-% LocalWords: displaymath noindent ignorespaces
diff --git a/macros/latex/contrib/stex/sty/sproof/sproof.ins b/macros/latex/contrib/stex/sty/sproof/sproof.ins
deleted file mode 100644
index e5f5198021..0000000000
--- a/macros/latex/contrib/stex/sty/sproof/sproof.ins
+++ /dev/null
@@ -1,30 +0,0 @@
-%%
-%% This file generates files required to use the ed package.
-%% At your command prompt write
-%%
-%% latex sproof.ins
-%%
-%% Copyright(c) 2005 Michael Kohlhase
-%%
-%% This file is distributed under the terms of the LaTeX Project Public
-%% License from CTAN archives in directory macros/latex/base/lppl.txt.
-%% Either version 1.0 or, at your option, any later version.
-%%
-\input docstrip
-\preamble
-\endpreamble
-
-%\usedir{tex/latex/listings}
-\keepsilent
-\askforoverwritefalse
-
-% generate base package
-\generate{\file{sproof.sty}{\from{sproof.dtx}{package}}}
-
-\Msg{*}
-\Msg{* You probably need to move the generated style files into a directory searched by TeX.}
-\Msg{*}
-\Msg{* And don't forget to refresh your filename database}
-\Msg{* if your TeX distribution uses such a database.}
-\Msg{*}
-\endbatchfile
diff --git a/macros/latex/contrib/stex/sty/sproof/sproof.pdf b/macros/latex/contrib/stex/sty/sproof/sproof.pdf
deleted file mode 100644
index 9478c6f254..0000000000
--- a/macros/latex/contrib/stex/sty/sproof/sproof.pdf
+++ /dev/null
Binary files differ