summaryrefslogtreecommitdiff
path: root/Master/texmf-dist/doc/latex/stex/example/paper/paper.tex
diff options
context:
space:
mode:
Diffstat (limited to 'Master/texmf-dist/doc/latex/stex/example/paper/paper.tex')
-rw-r--r--Master/texmf-dist/doc/latex/stex/example/paper/paper.tex149
1 files changed, 149 insertions, 0 deletions
diff --git a/Master/texmf-dist/doc/latex/stex/example/paper/paper.tex b/Master/texmf-dist/doc/latex/stex/example/paper/paper.tex
new file mode 100644
index 00000000000..5451a828f20
--- /dev/null
+++ b/Master/texmf-dist/doc/latex/stex/example/paper/paper.tex
@@ -0,0 +1,149 @@
+\documentclass{omdoc}
+\usepackage[showmods]{stex}
+\usepackage{amssymb}
+\usepackage{alltt}
+\usepackage{hyperref}
+\usepackage{listings}
+\def\omdoc{OMDoc}
+\def\latexml{LaTeXML}
+\defpath{backmods}{../background}
+%% defining the author metadata
+\WAperson[id=miko,
+ affiliation=JUB,
+ url=http://kwarc.info/kohlhase]
+ {Michael Kohlhase}
+\WAinstitution[id=JUB,
+ url=http://jacobs-university.de,
+ streetaddress={Campus Ring 1},
+ townzip={28759 Bremen},
+ countryshort=D,
+ country=Germany,
+ type=University,
+ acronym=JACU,
+ shortname=Jacobs Univ.]
+ {Jacobs University Bremen}
+
+\begin{document}
+
+% metadata and title page
+% \begin{DCmetadata}[maketitle]
+% \DCMcreators{miko}
+% \DCMrights{Copyright (c) 2009 Michael Kohlhase}
+% \DCMtitle{An example of semantic Markup in {\sTeX}}
+% \DCMabstract{In this note we give an example of semantic markup in {\sTeX}:
+% Continuous and differentiable functions are introduced using real numbers, sets and
+% functions as an assumed background.}
+% \end{DCmetadata}
+
+\inputref{intro}
+
+\begin{omgroup}[id=sec.math]{Mathematical Content}
+ \begin{omgroup}{Calculus}
+ We present some standard mathematical definitions, here from calculus.
+ \inputref{continuous}
+ \inputref{differentiable}
+\end{omgroup}
+
+\begin{omgroup}[id=sec.math]{A Theory Graph for Elementary Algebra}
+ Here we show an example for more advanced theory graph manipulations, in particular
+ imports via morphisms.
+
+\begin{module}[id=magma]
+ \importmodule[\backmods{functions}]{functions}
+ \symdef{magbase}{G}
+ \symdef[name=magmaop]{magmaopOp}{\circ}
+ \symdef{magmaop}[2]{\infix\magmaopOp{#1}{#2}}
+ \begin{definition}[id=magma.def]
+ A \defi{magma} is a structure $\tup{\magbase,\magmaopOp}$, such that $\magbase$ is
+ closed under the operation $\fun\magmaopOp{\cart{\magbase,\magbase}}\magbase$.
+ \end{definition}
+\end{module}
+
+\begin{module}[id=semigroup]
+ \importmodule{magma}
+ \begin{definition}[id=semigroup.def]
+ A \trefi[magma]{magma} $\tup{\magbase,\magmaopOp}$, is called a \defi{semigroup}, iff
+ $\magmaopOp$ is associative.
+ \end{definition}
+\end{module}
+
+\begin{module}[id=monoid]
+ \importmodule{semigroup}
+ \symdef{monneut}{e}
+ \symdef{noneut}[1]{#1^*}
+ \begin{definition}[id=monoid.def]
+ A \defi{monoid} is a structure $\tup{\magbase,\magmaopOp,\monneut}$, such that
+ $\tup{\magbase,\magmaopOp}$ is a \trefi[semigroup]{semigroup} and $\monneut$ is a
+ \defii{neutral}{element}, i.e. that $\magmaop{x}\monneut=x$ for all $\inset{x}\magbase$.
+ \end{definition}
+
+ \begin{definition}[id=noneut.def]
+ In a monoid $\tup{\magbase,\magmaopOp,\monneut}$, we use denote the set
+ $\setst{\inset{x}S}{x\ne\monneut}$ with $\noneut{S}$.
+ \end{definition}
+\end{module}
+
+\begin{module}[id=group]
+ \importmodule{monoid}
+ \symdef{ginvOp}{i}
+ \symdef{ginv}[1]{\prefix\ginvOp{#1}}
+ \begin{definition}[id=group.def]
+ A \defi{group} is a structure $\tup{\magbase,\magmaopOp,\monneut,\ginvOp}$, such that
+ $\tup{\magbase,\magmaopOp,\monneut}$ is a \trefi[monoid]{monoid} and $\ginvOp$ acts as
+ a \defi{inverse}, i.e. that $\magmaop{x}{\ginv{x}}=\monneut$ for all
+ $\inset{x}\magbase$.
+ \end{definition}
+\end{module}
+
+\begin{module}[id=cgroup]
+\importmodule{group}
+\begin{definition}[id=cgroup.def]
+ We call a \trefi[group]{group} $\tup{\magbase,\magmaopOp,\monneut,\ginvOp}$ a
+ \defii{commutative}{group}, iff $\magmaopOp$ is commutative.
+\end{definition}
+\end{module}
+
+\begin{module}[id=ring]
+\symdef{rbase}{R}
+\symdef[name=rtimes]{rtimesOp}{\cdot}
+\symdef{rtimes}[2]{\infix\rtimesOp{#1}{#2}}
+\symdef{rone}{1}
+\begin{importmodulevia}{monoid}
+ \vassign{rbase}\magbase
+ \vassign{rtimesOp}\magmaopOp
+ \vassign{rone}\monneut
+\end{importmodulevia}
+\symdef[name=rplus]{rplusOp}{+}
+\symdef{rplus}[2]{\infix\rplusOp{#1}{#2}}
+\symdef{rzero}{0}
+\symdef[name=rminus]{rminusOp}{-}
+\symdef{rminus}[1]{\prefix\rminusOp{#1}}
+\begin{importmodulevia}{cgroup}
+ \vassign{rplus}\magmaopOp
+ \vassign{rzero}\monneut
+ \vassign{rminusOp}\ginvOp
+\end{importmodulevia}
+\begin{definition}
+ A \defi{ring} is a structure $\tup{\rbase,\rplusOp,\rzero,\rtimesOp,\rone,\rminusOp}$,
+ such that $\tup{\noneut\rbase,\rtimesOp,\rone}$ is a monoid and
+ $\tup{\rbase,\rplusOp,\rzero,\rminusOp}$ is a commutative group.
+\end{definition}
+\end{module}
+\end{omgroup}
+\end{omgroup}
+
+\begin{omgroup}[id=concl]{Conclusion}
+ In this note we have given an example of standard mathematical markup and shown how a a
+ {\sTeX} collection can be set up for automation.
+\end{omgroup}
+\bibliographystyle{alpha}
+\bibliography{kwarc}
+\end{document}
+
+%%% Local Variables:
+%%% mode: LaTeX
+%%% TeX-master: t
+%%% End:
+
+% LocalWords: miko Makefiles tex contfuncs modf sms pdflatex latexml Makefile
+% LocalWords: latexmlpost omdoc STEXDIR BUTFILES DIRS