move generated files to document/ to avoid CVS file overwrite in generated/
cleanup (no generated root.pdf, session_graph.pdf etc)
--- a/doc-src/LaTeXsugar/IsaMakefile Sat Apr 30 02:43:45 2005 +0200
+++ b/doc-src/LaTeXsugar/IsaMakefile Sat Apr 30 02:45:17 2005 +0200
@@ -14,7 +14,7 @@
OUT = $(ISABELLE_OUTPUT)
LOG = $(OUT)/log
-USEDIR = $(ISATOOL) usedir -v true -i true -d pdf -D generated -H false
+USEDIR = $(ISATOOL) usedir -v true -i false -g false -d false -D document -H false
## Sugar
--- a/doc-src/LaTeXsugar/Makefile Sat Apr 30 02:43:45 2005 +0200
+++ b/doc-src/LaTeXsugar/Makefile Sat Apr 30 02:45:17 2005 +0200
@@ -8,7 +8,7 @@
## paths
-SRCPATH = Sugar/generated
+SRCPATH = Sugar/document
## dependencies
@@ -16,31 +16,31 @@
NAME = sugar
-FILES = Sugar/generated/root.tex Sugar/generated/root.bib \
- Sugar/generated/mathpartir.sty Sugar/generated/LaTeXsugar.tex \
- Sugar/generated/OptionalSugar.tex
+FILES = Sugar/document/root.tex Sugar/document/root.bib \
+ Sugar/document/mathpartir.sty Sugar/document/LaTeXsugar.tex \
+ Sugar/document/OptionalSugar.tex
-GARBAGE = Sugar/generated/*.aux Sugar/generated/*.log Sugar/generated/*.toc \
- Sugar/generated/*.idx Sugar/generated/*.bbl Sugar/generated/*.blg \
- Sugar/generated/*.out
+GARBAGE = Sugar/document/*.aux Sugar/document/*.log Sugar/document/*.toc \
+ Sugar/document/*.idx Sugar/document/*.bbl Sugar/document/*.blg \
+ Sugar/document/*.out
dvi: $(NAME).dvi
$(NAME).dvi: $(FILES)
- cd Sugar/generated; \
+ cd Sugar/document; \
$(LATEX) root; \
$(BIBTEX) root; \
$(LATEX) root; \
$(LATEX) root
- cp $(SRCPATH)/root.dvi $(NAME).dvi
+ mv $(SRCPATH)/root.dvi $(NAME).dvi
pdf: $(NAME).pdf
$(NAME).pdf: $(FILES)
- cd Sugar/generated; \
+ cd Sugar/document; \
$(PDFLATEX) root; \
$(BIBTEX) root; \
$(PDFLATEX) root; \
$(PDFLATEX) root
- cp $(SRCPATH)/root.pdf $(NAME).pdf
+ mv $(SRCPATH)/root.pdf $(NAME).pdf
--- a/doc-src/LaTeXsugar/Sugar/generated/Sugar.tex Sat Apr 30 02:43:45 2005 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,363 +0,0 @@
-%
-\begin{isabellebody}%
-\def\isabellecontext{Sugar}%
-\isamarkupfalse%
-%
-\isamarkupsection{Introduction%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-This document is for those Isabelle users who have mastered
-the art of mixing \LaTeX\ text and Isabelle theories and never want to
-typeset a theorem by hand anymore because they have experienced the
-bliss of writing \verb!@!\verb!{thm[display]setsum_cartesian_product[no_vars]}!
-and seeing Isabelle typeset it for them:
-\begin{isabelle}%
-{\isacharparenleft}{\isasymSum}x{\isasymin}A{\isachardot}\ {\isasymSum}y{\isasymin}B{\isachardot}\ f\ x\ y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isasymSum}z{\isasymin}A\ {\isasymtimes}\ B{\isachardot}\ f\ {\isacharparenleft}fst\ z{\isacharparenright}\ {\isacharparenleft}snd\ z{\isacharparenright}{\isacharparenright}%
-\end{isabelle}
-No typos, no omissions, no sweat.
-If you have not experienced that joy, read Chapter 4, \emph{Presenting
-Theories}, \cite{LNCS2283} first.
-
-If you have mastered the art of Isabelle's \emph{antiquotations},
-i.e.\ things like the above \verb!@!\verb!{thm...}!, beware: in your vanity
-you may be tempted to think that all readers of the stunning ps or pdf
-documents you can now produce at the drop of a hat will be struck with
-awe at the beauty unfolding in front of their eyes. Until one day you
-come across that very critical of readers known as the ``common referee''.
-He has the nasty habit of refusing to understand unfamiliar notation
-like Isabelle's infamous \isa{{\isasymlbrakk}\ {\isasymrbrakk}\ {\isasymLongrightarrow}} no matter how many times you
-explain it in your paper. Even worse, he thinks that using \isa{{\isasymlbrakk}\ {\isasymrbrakk}} for anything other than denotational semantics is a cardinal sin
-that must be punished by instant rejection.
-
-
-This document shows you how to make Isabelle and \LaTeX\ cooperate to
-produce ordinary looking mathematics that hides the fact that it was
-typeset by a machine. You merely need to load the right files:
-\begin{itemize}
-\item Import theory \texttt{LaTeXsugar} in the header of your own
-theory. You may also want bits of \texttt{OptionalSugar}, which you can
-copy selectively into your own theory or import as a whole. Both
-theories live in \texttt{HOL/Library} and are found automatically.
-
-\item Should you need additional \LaTeX\ packages (the text will tell
-you so), you include them at the beginning of your \LaTeX\ document,
-typically in \texttt{root.tex}.
-\end{itemize}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsection{HOL syntax%
-}
-\isamarkuptrue%
-%
-\isamarkupsubsection{Logic%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-The predefined constructs \isa{if}, \isa{let} and
-\isa{case} are set in sans serif font to distinguish them from
-other functions. This improves readability:
-\begin{itemize}
-\item \isa{\textsf{if}\ b\ \textsf{then}\ e\isactrlisub {\isadigit{1}}\ \textsf{else}\ e\isactrlisub {\isadigit{2}}} instead of \isa{if\ b\ then\ e\isactrlisub {\isadigit{1}}\ else\ e\isactrlisub {\isadigit{2}}}.
-\item \isa{\textsf{let}\ x\ {\isacharequal}\ e\isactrlisub {\isadigit{1}}\ \textsf{in}\ e\isactrlisub {\isadigit{2}}} instead of \isa{let\ x\ {\isacharequal}\ e\isactrlisub {\isadigit{1}}\ in\ e\isactrlisub {\isadigit{2}}}.
-\item \isa{\textsf{case}\ x\ \textsf{of}\ True\ {\isasymRightarrow}\ e\isactrlisub {\isadigit{1}}\ {\isacharbar}\ False\ {\isasymRightarrow}\ e\isactrlisub {\isadigit{2}}} instead of\\
- \isa{case\ x\ of\ True\ {\isasymRightarrow}\ e\isactrlisub {\isadigit{1}}\ {\isacharbar}\ False\ {\isasymRightarrow}\ e\isactrlisub {\isadigit{2}}}.
-\end{itemize}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Sets%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-Although set syntax in HOL is already close to
-standard, we provide a few further improvements:
-\begin{itemize}
-\item \isa{{\isacharbraceleft}x\ {\isacharbar}\ P{\isacharbraceright}} instead of \isa{{\isacharbraceleft}x{\isachardot}\ P{\isacharbraceright}}.
-\item \isa{{\isasymemptyset}} instead of \isa{{\isacharbraceleft}{\isacharbraceright}}.
-\item \isa{{\isacharbraceleft}a{\isacharcomma}\ b{\isacharcomma}\ c{\isacharbraceright}\ {\isasymunion}\ M} instead of \isa{insert\ a\ {\isacharparenleft}insert\ b\ {\isacharparenleft}insert\ c\ M{\isacharparenright}{\isacharparenright}}.
-\end{itemize}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Lists%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-If lists are used heavily, the following notations increase readability:
-\begin{itemize}
-\item \isa{x{\isasymcdot}xs} instead of \isa{x\ {\isacharhash}\ xs}.
- Exceptionally, \isa{x{\isasymcdot}xs} is also input syntax.
-If you prefer more space around the $\cdot$ you have to redefine
-\verb!\isasymcdot! in \LaTeX:
-\verb!\renewcommand{\isasymcdot}{\isamath{\,\cdot\,}}!
-
-\item \isa{{\isacharbar}xs{\isacharbar}} instead of \isa{length\ xs}.
-\item \isa{xs\ensuremath{_{[\mathit{n}]}}} instead of \isa{nth\ xs\ n},
- the $n$th element of \isa{xs}.
-
-\item The \isa{{\isacharat}} operation associates implicitly to the right,
-which leads to unpleasant line breaks if the term is too long for one
-line. To avoid this, \texttt{OptionalSugar} contains syntax to group
-\isa{{\isacharat}}-terms to the left before printing, which leads to better
-line breaking behaviour:
-\begin{isabelle}%
-term\isactrlisub {\isadigit{0}}\ \isacharat\ term\isactrlisub {\isadigit{1}}\ \isacharat\ term\isactrlisub {\isadigit{2}}\ \isacharat\ term\isactrlisub {\isadigit{3}}\ \isacharat\ term\isactrlisub {\isadigit{4}}\ \isacharat\ term\isactrlisub {\isadigit{5}}\ \isacharat\ term\isactrlisub {\isadigit{6}}\ \isacharat\ term\isactrlisub {\isadigit{7}}\ \isacharat\ term\isactrlisub {\isadigit{8}}\ \isacharat\ term\isactrlisub {\isadigit{9}}\ \isacharat\ term\isactrlisub {\isadigit{1}}\isactrlisub {\isadigit{0}}%
-\end{isabelle}
-
-\end{itemize}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsection{Printing theorems%
-}
-\isamarkuptrue%
-%
-\isamarkupsubsection{Question marks%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-If you print anything, especially theorems, containing
-schematic variables they are prefixed with a question mark:
-\verb!@!\verb!{thm conjI}! results in \isa{{\isasymlbrakk}{\isacharquery}P{\isacharsemicolon}\ {\isacharquery}Q{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}P\ {\isasymand}\ {\isacharquery}Q}. Most of the time
-you would rather not see the question marks. There is an attribute
-\verb!no_vars! that you can attach to the theorem that turns its
-schematic into ordinary free variables: \verb!@!\verb!{thm conjI[no_vars]}!
-results in \isa{{\isasymlbrakk}P{\isacharsemicolon}\ Q{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ {\isasymand}\ Q}.
-
-This \verb!no_vars! business can become a bit tedious.
-If you would rather never see question marks, simply put
-\begin{verbatim}
-reset show_var_qmarks;
-\end{verbatim}
-at the beginning of your file \texttt{ROOT.ML}.
-The rest of this document is produced with this flag reset.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isamarkupfalse%
-%
-\isamarkupsubsection{Inference rules%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-To print theorems as inference rules you need to include Didier
-R\'emy's \texttt{mathpartir} package~\cite{mathpartir}
-for typesetting inference rules in your \LaTeX\ file.
-
-Writing \verb!@!\verb!{thm[mode=Rule] conjI}! produces
-\isa{\mbox{}\inferrule{\mbox{P}\\\ \mbox{Q}}{\mbox{P\ {\isasymand}\ Q}}}, even in the middle of a sentence.
-If you prefer your inference rule on a separate line, maybe with a name,
-\begin{center}
-\isa{\mbox{}\inferrule{\mbox{P}\\\ \mbox{Q}}{\mbox{P\ {\isasymand}\ Q}}} {\sc conjI}
-\end{center}
-is produced by
-\begin{quote}
-\verb!\begin{center}!\\
-\verb!@!\verb!{thm[mode=Rule] conjI} {\sc conjI}!\\
-\verb!\end{center}!
-\end{quote}
-It is not recommended to use the standard \texttt{display} attribute
-together with \texttt{Rule} because centering does not work and because
-the line breaking mechanisms of \texttt{display} and \texttt{mathpartir} can
-clash.
-
-Of course you can display multiple rules in this fashion:
-\begin{quote}
-\verb!\begin{center}\isastyle!\\
-\verb!@!\verb!{thm[mode=Rule] conjI} {\sc conjI} \\[1ex]!\\
-\verb!@!\verb!{thm[mode=Rule] conjE} {\sc disjI$_1$} \qquad!\\
-\verb!@!\verb!{thm[mode=Rule] disjE} {\sc disjI$_2$}!\\
-\verb!\end{center}!
-\end{quote}
-yields
-\begin{center}\isastyle
-\isa{\mbox{}\inferrule{\mbox{P}\\\ \mbox{Q}}{\mbox{P\ {\isasymand}\ Q}}} {\sc conjI} \\[1ex]
-\isa{\mbox{}\inferrule{\mbox{P}}{\mbox{P\ {\isasymor}\ Q}}} {\sc disjI$_1$} \qquad
-\isa{\mbox{}\inferrule{\mbox{Q}}{\mbox{P\ {\isasymor}\ Q}}} {\sc disjI$_2$}
-\end{center}
-Note that we included \verb!\isastyle! to obtain
-the smaller font that otherwise comes only with \texttt{display}.
-
-The \texttt{mathpartir} package copes well if there are too many
-premises for one line:
-\begin{center}
-\isa{\mbox{}\inferrule{\mbox{A\ {\isasymlongrightarrow}\ B}\\\ \mbox{B\ {\isasymlongrightarrow}\ C}\\\ \mbox{C\ {\isasymlongrightarrow}\ D}\\\ \mbox{D\ {\isasymlongrightarrow}\ E}\\\ \mbox{E\ {\isasymlongrightarrow}\ F}\\\ \mbox{F\ {\isasymlongrightarrow}\ G}\\\ \mbox{G\ {\isasymlongrightarrow}\ H}\\\ \mbox{H\ {\isasymlongrightarrow}\ I}\\\ \mbox{I\ {\isasymlongrightarrow}\ J}\\\ \mbox{J\ {\isasymlongrightarrow}\ K}}{\mbox{A\ {\isasymlongrightarrow}\ K}}}
-\end{center}
-
-Limitations: 1. Premises and conclusion must each not be longer than
-the line. 2. Premises that are \isa{{\isasymLongrightarrow}}-implications are again
-displayed with a horizontal line, which looks at least unusual.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{If-then%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-If you prefer a fake ``natural language'' style you can produce
-the body of
-\newtheorem{theorem}{Theorem}
-\begin{theorem}
-\isa{{\rmfamily\upshape\normalsize{}If\,}\ \mbox{i\ {\isasymle}\ j}\ {\rmfamily\upshape\normalsize \,and\,}\ \mbox{j\ {\isasymle}\ k}\ {\rmfamily\upshape\normalsize \,then\,}\ i\ {\isasymle}\ k{\isachardot}}
-\end{theorem}
-by typing
-\begin{quote}
-\verb!@!\verb!{thm[mode=IfThen] le_trans}!
-\end{quote}
-
-In order to prevent odd line breaks, the premises are put into boxes.
-At times this is too drastic:
-\begin{theorem}
-\isa{{\rmfamily\upshape\normalsize{}If\,}\ \mbox{longpremise}\ {\rmfamily\upshape\normalsize \,and\,}\ \mbox{longerpremise}\ {\rmfamily\upshape\normalsize \,and\,}\ \mbox{P\ {\isacharparenleft}f\ {\isacharparenleft}f\ {\isacharparenleft}f\ {\isacharparenleft}f\ {\isacharparenleft}f\ {\isacharparenleft}f\ {\isacharparenleft}f\ {\isacharparenleft}f\ {\isacharparenleft}f\ x{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharparenright}}\ {\rmfamily\upshape\normalsize \,and\,}\ \mbox{longestpremise}\ {\rmfamily\upshape\normalsize \,then\,}\ conclusion{\isachardot}}
-\end{theorem}
-In which case you should use \texttt{mode=IfThenNoBox} instead of
-\texttt{mode=IfThen}:
-\begin{theorem}
-\isa{{\rmfamily\upshape\normalsize{}If\,}\ longpremise\ {\rmfamily\upshape\normalsize \,and\,}\ longerpremise\ {\rmfamily\upshape\normalsize \,and\,}\ P\ {\isacharparenleft}f\ {\isacharparenleft}f\ {\isacharparenleft}f\ {\isacharparenleft}f\ {\isacharparenleft}f\ {\isacharparenleft}f\ {\isacharparenleft}f\ {\isacharparenleft}f\ {\isacharparenleft}f\ x{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharparenright}\ {\rmfamily\upshape\normalsize \,and\,}\ longestpremise\ {\rmfamily\upshape\normalsize \,then\,}\ conclusion{\isachardot}}
-\end{theorem}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Definitions and Equations%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-The \verb!thm! antiquotation works nicely for proper theorems, but
- sets of equations as used in definitions are more difficult to
- typeset nicely: for some reason people tend to prefer aligned
- \isa{{\isacharequal}} signs.
-
- Isabelle2005 has a nice mechanism for this, namely the two
- antiquotations \verb!@!\verb!{lhs thm}! and \verb!@!\verb!{rhs thm}!.
-
- \begin{center}
- \begin{tabular}{l@ {~~\isa{{\isacharequal}}~~}l}
- \isa{foldl\ f\ a\ {\isacharbrackleft}{\isacharbrackright}} & \isa{a}\\
- \isa{foldl\ f\ a\ {\isacharparenleft}x{\isasymcdot}xs{\isacharparenright}} & \isa{foldl\ f\ {\isacharparenleft}f\ a\ x{\isacharparenright}\ xs}
- \end{tabular}
- \end{center}
-
- \noindent
- is produced by the following code:
-
-\begin{quote}
- \verb!\begin{center}!\\
- \verb!\begin{tabular}{l@ {~~!\verb!@!\verb!{text "="}~~}l}!\\
- \verb!@!\verb!{lhs foldl_Nil} & @!\verb!{rhs foldl_Nil}!\\
- \verb!@!\verb!{lhs foldl_Cons} & @!\verb!{rhs foldl_Cons}!\\
- \verb!\end{tabular}!\\
- \verb!\end{center}!
-\end{quote}
-
- \noindent
- Note the space between \verb!@! and \verb!{! in the tabular argument.
- It prevents Isabelle from interpreting \verb!@ {~~...~~}!
- as antiquotation. \verb!@!\verb!{lhs thm}! and \verb!@!\verb!{rhs thm}!
- try to be smart about the interpretation of the theorem they
- print, they work just as well for meta equality \isa{{\isasymequiv}} and other
- binary operators like \isa{{\isacharless}}.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Patterns%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-Sometimes functions ignore one or more of their
- arguments and some functional languages have nice
- syntax for that as in \isa{hd\ {\isacharparenleft}x{\isasymcdot}\_{\isacharparenright}\ {\isacharequal}\ x}.
-
- You can simulate this in Isabelle by instantiating the \isa{xs} in
- definition \mbox{\isa{hd\ {\isacharparenleft}x{\isasymcdot}xs{\isacharparenright}\ {\isacharequal}\ x}} with a constant \isa{DUMMY} that
- is printed as \isa{\_}. The code for the pattern above is
- \verb!@!\verb!{thm hd.simps [where xs=DUMMY]}!.
-
- You can drive this game even further and extend the syntax of let
- bindings such that certain functions like \isa{fst}, \isa{hd},
- etc.\ are printed as patterns. \texttt{OptionalSugar} provides the
- following:
-
- \begin{center}
- \begin{tabular}{l@ {~~produced by~~}l}
- \isa{\textsf{let}\ {\isacharparenleft}x{\isacharcomma}\ \_{\isacharparenright}\ {\isacharequal}\ p\ \textsf{in}\ t} & \verb!@!\verb!{term "let x = fst p in t"}!\\
- \isa{\textsf{let}\ {\isacharparenleft}\_{\isacharcomma}\ x{\isacharparenright}\ {\isacharequal}\ p\ \textsf{in}\ t} & \verb!@!\verb!{term "let x = snd p in t"}!\\
- \isa{\textsf{let}\ x{\isasymcdot}\_\ {\isacharequal}\ xs\ \textsf{in}\ t} & \verb!@!\verb!{term "let x = hd xs in t"}!\\
- \isa{\textsf{let}\ \_{\isasymcdot}x\ {\isacharequal}\ xs\ \textsf{in}\ t} & \verb!@!\verb!{term "let x = tl xs in t"}!\\
- \isa{\textsf{let}\ Some\ x\ {\isacharequal}\ y\ \textsf{in}\ t} & \verb!@!\verb!{term "let x = the y in t"}!\\
- \end{tabular}
- \end{center}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Proofs%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-Full proofs, even if written in beautiful Isar style, are likely to
- be too long and detailed to be included in conference papers, but
- some key lemmas might be of interest.
-
- It is usually easiest to put them in figures like the one in Fig.\
- \ref{fig:proof}. This was achieved with the \isakeyword{text\_raw}
- command:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\begin{figure}
- \begin{center}\begin{minipage}{0.6\textwidth}
- \isastyle\isamarkuptrue
-\isacommand{lemma}\ True\isanewline
-\isamarkupfalse%
-\isacommand{proof}\ {\isacharminus}\isanewline
-\ \ %
-\isamarkupcmt{pretty trivial%
-}
-\isanewline
-\ \ \isamarkupfalse%
-\isacommand{show}\ True\ \isamarkupfalse%
-\isacommand{by}\ force\isanewline
-\isamarkupfalse%
-\isacommand{qed}\isamarkupfalse%
-%
-\end{minipage}\end{center}
- \caption{Example proof in a figure.}\label{fig:proof}
- \end{figure}
-%
-\begin{isamarkuptext}%
-\begin{quote}
-\small
-\verb!text_raw {!\verb!*!\\
-\verb! \begin{figure}!\\
-\verb! \begin{center}\begin{minipage}{0.6\textwidth}!\\
-\verb! \isastyle\isamarkuptrue!\\
-\verb!*!\verb!}!\\
-\verb!lemma True!\\
-\verb!proof -!\\
-\verb! -- "pretty trivial"!\\
-\verb! show True by force!\\
-\verb!qed!\\
-\verb!text_raw {!\verb!*!\\
-\verb! \end{minipage}\end{center}!\\
-\verb! \caption{Example proof in a figure.}\label{fig:proof}!\\
-\verb! \end{figure}!\\
-\verb!*!\verb!}!
-\end{quote}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isamarkupfalse%
-\end{isabellebody}%
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: "root"
-%%% End:
--- a/doc-src/LaTeXsugar/Sugar/generated/isabelle.sty Sat Apr 30 02:43:45 2005 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,164 +0,0 @@
-%%
-%% Author: Markus Wenzel, TU Muenchen
-%%
-%% macros for Isabelle generated LaTeX output
-%%
-
-%%% Simple document preparation (based on theory token language and symbols)
-
-% isabelle environments
-
-\newcommand{\isabellecontext}{UNKNOWN}
-
-\newcommand{\isastyle}{\small\tt\slshape}
-\newcommand{\isastyleminor}{\small\tt\slshape}
-\newcommand{\isastylescript}{\footnotesize\tt\slshape}
-\newcommand{\isastyletext}{\normalsize\rm}
-\newcommand{\isastyletxt}{\rm}
-\newcommand{\isastylecmt}{\rm}
-
-%symbol markup -- \emph achieves decent spacing via italic corrections
-\newcommand{\isamath}[1]{\emph{$#1$}}
-\newcommand{\isatext}[1]{\emph{#1}}
-\newcommand{\isascriptstyle}{\def\isamath##1{##1}\def\isatext##1{\mbox{\isastylescript##1}}}
-\newcommand{\isactrlsub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
-\newcommand{\isactrlsup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
-\newcommand{\isactrlisub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
-\newcommand{\isactrlisup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
-\newcommand{\isactrlbsub}{\emph\bgroup\begin{math}{}\sb\bgroup\mbox\bgroup\isastylescript}
-\newcommand{\isactrlesub}{\egroup\egroup\end{math}\egroup}
-\newcommand{\isactrlbsup}{\emph\bgroup\begin{math}{}\sp\bgroup\mbox\bgroup\isastylescript}
-\newcommand{\isactrlesup}{\egroup\egroup\end{math}\egroup}
-\newcommand{\isactrlbold}[1]{{\bfseries\upshape\boldmath#1}}
-
-
-\newdimen\isa@parindent\newdimen\isa@parskip
-
-\newenvironment{isabellebody}{%
-\isamarkuptrue\par%
-\isa@parindent\parindent\parindent0pt%
-\isa@parskip\parskip\parskip0pt%
-\isastyle}{\par}
-
-\newenvironment{isabelle}
-{\begin{trivlist}\begin{isabellebody}\item\relax}
-{\end{isabellebody}\end{trivlist}}
-
-\newcommand{\isa}[1]{\emph{\isastyleminor #1}}
-
-\newcommand{\isaindent}[1]{\hphantom{#1}}
-\newcommand{\isanewline}{\mbox{}\par\mbox{}}
-\newcommand{\isasep}{} % override with e.g. \renewcommand{\isasep}{\vspace{1ex}}
-\newcommand{\isadigit}[1]{#1}
-
-\chardef\isacharbang=`\!
-\chardef\isachardoublequote=`\"
-\chardef\isacharhash=`\#
-\chardef\isachardollar=`\$
-\chardef\isacharpercent=`\%
-\chardef\isacharampersand=`\&
-\chardef\isacharprime=`\'
-\chardef\isacharparenleft=`\(
-\chardef\isacharparenright=`\)
-\chardef\isacharasterisk=`\*
-\chardef\isacharplus=`\+
-\chardef\isacharcomma=`\,
-\chardef\isacharminus=`\-
-\chardef\isachardot=`\.
-\chardef\isacharslash=`\/
-\chardef\isacharcolon=`\:
-\chardef\isacharsemicolon=`\;
-\chardef\isacharless=`\<
-\chardef\isacharequal=`\=
-\chardef\isachargreater=`\>
-\chardef\isacharquery=`\?
-\chardef\isacharat=`\@
-\chardef\isacharbrackleft=`\[
-\chardef\isacharbackslash=`\\
-\chardef\isacharbrackright=`\]
-\chardef\isacharcircum=`\^
-\chardef\isacharunderscore=`\_
-\chardef\isacharbackquote=`\`
-\chardef\isacharbraceleft=`\{
-\chardef\isacharbar=`\|
-\chardef\isacharbraceright=`\}
-\chardef\isachartilde=`\~
-
-
-% keyword and section markup
-
-\newcommand{\isakeywordcharunderscore}{\_}
-\newcommand{\isakeyword}[1]
-{\emph{\bf\def\isachardot{.}\def\isacharunderscore{\isakeywordcharunderscore}%
-\def\isacharbraceleft{\{}\def\isacharbraceright{\}}#1}}
-\newcommand{\isacommand}[1]{\isakeyword{#1}}
-
-\newcommand{\isamarkupheader}[1]{\section{#1}}
-\newcommand{\isamarkupchapter}[1]{\chapter{#1}}
-\newcommand{\isamarkupsection}[1]{\section{#1}}
-\newcommand{\isamarkupsubsection}[1]{\subsection{#1}}
-\newcommand{\isamarkupsubsubsection}[1]{\subsubsection{#1}}
-\newcommand{\isamarkupsect}[1]{\section{#1}}
-\newcommand{\isamarkupsubsect}[1]{\subsection{#1}}
-\newcommand{\isamarkupsubsubsect}[1]{\subsubsection{#1}}
-
-\newif\ifisamarkup
-\newcommand{\isabeginpar}{\par\ifisamarkup\relax\else\medskip\fi}
-\newcommand{\isaendpar}{\par\medskip}
-\newenvironment{isapar}{\parindent\isa@parindent\parskip\isa@parskip\isabeginpar}{\isaendpar}
-\newenvironment{isamarkuptext}{\isastyletext\begin{isapar}}{\end{isapar}}
-\newenvironment{isamarkuptxt}{\isastyletxt\begin{isapar}}{\end{isapar}}
-\newcommand{\isamarkupcmt}[1]{{\isastylecmt--- #1}}
-
-
-% alternative styles
-
-\newcommand{\isabellestyle}{}
-\def\isabellestyle#1{\csname isabellestyle#1\endcsname}
-
-\newcommand{\isabellestylett}{%
-\renewcommand{\isastyle}{\small\tt}%
-\renewcommand{\isastyleminor}{\small\tt}%
-\renewcommand{\isastylescript}{\footnotesize\tt}%
-}
-\newcommand{\isabellestyleit}{%
-\renewcommand{\isastyle}{\small\it}%
-\renewcommand{\isastyleminor}{\it}%
-\renewcommand{\isastylescript}{\footnotesize\it}%
-\renewcommand{\isakeywordcharunderscore}{\mbox{-}}%
-\renewcommand{\isacharbang}{\isamath{!}}%
-\renewcommand{\isachardoublequote}{}%
-\renewcommand{\isacharhash}{\isamath{\#}}%
-\renewcommand{\isachardollar}{\isamath{\$}}%
-\renewcommand{\isacharpercent}{\isamath{\%}}%
-\renewcommand{\isacharampersand}{\isamath{\&}}%
-\renewcommand{\isacharprime}{\isamath{\mskip2mu{'}\mskip-2mu}}%
-\renewcommand{\isacharparenleft}{\isamath{(}}%
-\renewcommand{\isacharparenright}{\isamath{)}}%
-\renewcommand{\isacharasterisk}{\isamath{*}}%
-\renewcommand{\isacharplus}{\isamath{+}}%
-\renewcommand{\isacharcomma}{\isamath{\mathord,}}%
-\renewcommand{\isacharminus}{\isamath{-}}%
-\renewcommand{\isachardot}{\isamath{\mathord.}}%
-\renewcommand{\isacharslash}{\isamath{/}}%
-\renewcommand{\isacharcolon}{\isamath{\mathord:}}%
-\renewcommand{\isacharsemicolon}{\isamath{\mathord;}}%
-\renewcommand{\isacharless}{\isamath{<}}%
-\renewcommand{\isacharequal}{\isamath{=}}%
-\renewcommand{\isachargreater}{\isamath{>}}%
-\renewcommand{\isacharat}{\isamath{@}}%
-\renewcommand{\isacharbrackleft}{\isamath{[}}%
-\renewcommand{\isacharbrackright}{\isamath{]}}%
-\renewcommand{\isacharunderscore}{\mbox{-}}%
-\renewcommand{\isacharbraceleft}{\isamath{\{}}%
-\renewcommand{\isacharbar}{\isamath{\mid}}%
-\renewcommand{\isacharbraceright}{\isamath{\}}}%
-\renewcommand{\isachartilde}{\isamath{{}\sp{\sim}}}%
-}
-
-\newcommand{\isabellestylesl}{%
-\isabellestyleit%
-\renewcommand{\isastyle}{\small\sl}%
-\renewcommand{\isastyleminor}{\sl}%
-\renewcommand{\isastylescript}{\footnotesize\sl}%
-}
--- a/doc-src/LaTeXsugar/Sugar/generated/isabellesym.sty Sat Apr 30 02:43:45 2005 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,359 +0,0 @@
-%%
-%% Author: Markus Wenzel, TU Muenchen
-%%
-%% definitions of standard Isabelle symbols
-%%
-
-% symbol definitions
-
-\newcommand{\isasymzero}{\isamath{\mathbf{0}}} %requires amssymb
-\newcommand{\isasymone}{\isamath{\mathbf{1}}} %requires amssymb
-\newcommand{\isasymtwo}{\isamath{\mathbf{2}}} %requires amssymb
-\newcommand{\isasymthree}{\isamath{\mathbf{3}}} %requires amssymb
-\newcommand{\isasymfour}{\isamath{\mathbf{4}}} %requires amssymb
-\newcommand{\isasymfive}{\isamath{\mathbf{5}}} %requires amssymb
-\newcommand{\isasymsix}{\isamath{\mathbf{6}}} %requires amssymb
-\newcommand{\isasymseven}{\isamath{\mathbf{7}}} %requires amssymb
-\newcommand{\isasymeight}{\isamath{\mathbf{8}}} %requires amssymb
-\newcommand{\isasymnine}{\isamath{\mathbf{9}}} %requires amssymb
-\newcommand{\isasymA}{\isamath{\mathcal{A}}}
-\newcommand{\isasymB}{\isamath{\mathcal{B}}}
-\newcommand{\isasymC}{\isamath{\mathcal{C}}}
-\newcommand{\isasymD}{\isamath{\mathcal{D}}}
-\newcommand{\isasymE}{\isamath{\mathcal{E}}}
-\newcommand{\isasymF}{\isamath{\mathcal{F}}}
-\newcommand{\isasymG}{\isamath{\mathcal{G}}}
-\newcommand{\isasymH}{\isamath{\mathcal{H}}}
-\newcommand{\isasymI}{\isamath{\mathcal{I}}}
-\newcommand{\isasymJ}{\isamath{\mathcal{J}}}
-\newcommand{\isasymK}{\isamath{\mathcal{K}}}
-\newcommand{\isasymL}{\isamath{\mathcal{L}}}
-\newcommand{\isasymM}{\isamath{\mathcal{M}}}
-\newcommand{\isasymN}{\isamath{\mathcal{N}}}
-\newcommand{\isasymO}{\isamath{\mathcal{O}}}
-\newcommand{\isasymP}{\isamath{\mathcal{P}}}
-\newcommand{\isasymQ}{\isamath{\mathcal{Q}}}
-\newcommand{\isasymR}{\isamath{\mathcal{R}}}
-\newcommand{\isasymS}{\isamath{\mathcal{S}}}
-\newcommand{\isasymT}{\isamath{\mathcal{T}}}
-\newcommand{\isasymU}{\isamath{\mathcal{U}}}
-\newcommand{\isasymV}{\isamath{\mathcal{V}}}
-\newcommand{\isasymW}{\isamath{\mathcal{W}}}
-\newcommand{\isasymX}{\isamath{\mathcal{X}}}
-\newcommand{\isasymY}{\isamath{\mathcal{Y}}}
-\newcommand{\isasymZ}{\isamath{\mathcal{Z}}}
-\newcommand{\isasyma}{\isamath{\mathrm{a}}}
-\newcommand{\isasymb}{\isamath{\mathrm{b}}}
-\newcommand{\isasymc}{\isamath{\mathrm{c}}}
-\newcommand{\isasymd}{\isamath{\mathrm{d}}}
-\newcommand{\isasyme}{\isamath{\mathrm{e}}}
-\newcommand{\isasymf}{\isamath{\mathrm{f}}}
-\newcommand{\isasymg}{\isamath{\mathrm{g}}}
-\newcommand{\isasymh}{\isamath{\mathrm{h}}}
-\newcommand{\isasymi}{\isamath{\mathrm{i}}}
-\newcommand{\isasymj}{\isamath{\mathrm{j}}}
-\newcommand{\isasymk}{\isamath{\mathrm{k}}}
-\newcommand{\isasyml}{\isamath{\mathrm{l}}}
-\newcommand{\isasymm}{\isamath{\mathrm{m}}}
-\newcommand{\isasymn}{\isamath{\mathrm{n}}}
-\newcommand{\isasymo}{\isamath{\mathrm{o}}}
-\newcommand{\isasymp}{\isamath{\mathrm{p}}}
-\newcommand{\isasymq}{\isamath{\mathrm{q}}}
-\newcommand{\isasymr}{\isamath{\mathrm{r}}}
-\newcommand{\isasyms}{\isamath{\mathrm{s}}}
-\newcommand{\isasymt}{\isamath{\mathrm{t}}}
-\newcommand{\isasymu}{\isamath{\mathrm{u}}}
-\newcommand{\isasymv}{\isamath{\mathrm{v}}}
-\newcommand{\isasymw}{\isamath{\mathrm{w}}}
-\newcommand{\isasymx}{\isamath{\mathrm{x}}}
-\newcommand{\isasymy}{\isamath{\mathrm{y}}}
-\newcommand{\isasymz}{\isamath{\mathrm{z}}}
-\newcommand{\isasymAA}{\isamath{\mathfrak{A}}} %requires eufrak
-\newcommand{\isasymBB}{\isamath{\mathfrak{B}}} %requires eufrak
-\newcommand{\isasymCC}{\isamath{\mathfrak{C}}} %requires eufrak
-\newcommand{\isasymDD}{\isamath{\mathfrak{D}}} %requires eufrak
-\newcommand{\isasymEE}{\isamath{\mathfrak{E}}} %requires eufrak
-\newcommand{\isasymFF}{\isamath{\mathfrak{F}}} %requires eufrak
-\newcommand{\isasymGG}{\isamath{\mathfrak{G}}} %requires eufrak
-\newcommand{\isasymHH}{\isamath{\mathfrak{H}}} %requires eufrak
-\newcommand{\isasymII}{\isamath{\mathfrak{I}}} %requires eufrak
-\newcommand{\isasymJJ}{\isamath{\mathfrak{J}}} %requires eufrak
-\newcommand{\isasymKK}{\isamath{\mathfrak{K}}} %requires eufrak
-\newcommand{\isasymLL}{\isamath{\mathfrak{L}}} %requires eufrak
-\newcommand{\isasymMM}{\isamath{\mathfrak{M}}} %requires eufrak
-\newcommand{\isasymNN}{\isamath{\mathfrak{N}}} %requires eufrak
-\newcommand{\isasymOO}{\isamath{\mathfrak{O}}} %requires eufrak
-\newcommand{\isasymPP}{\isamath{\mathfrak{P}}} %requires eufrak
-\newcommand{\isasymQQ}{\isamath{\mathfrak{Q}}} %requires eufrak
-\newcommand{\isasymRR}{\isamath{\mathfrak{R}}} %requires eufrak
-\newcommand{\isasymSS}{\isamath{\mathfrak{S}}} %requires eufrak
-\newcommand{\isasymTT}{\isamath{\mathfrak{T}}} %requires eufrak
-\newcommand{\isasymUU}{\isamath{\mathfrak{U}}} %requires eufrak
-\newcommand{\isasymVV}{\isamath{\mathfrak{V}}} %requires eufrak
-\newcommand{\isasymWW}{\isamath{\mathfrak{W}}} %requires eufrak
-\newcommand{\isasymXX}{\isamath{\mathfrak{X}}} %requires eufrak
-\newcommand{\isasymYY}{\isamath{\mathfrak{Y}}} %requires eufrak
-\newcommand{\isasymZZ}{\isamath{\mathfrak{Z}}} %requires eufrak
-\newcommand{\isasymaa}{\isamath{\mathfrak{a}}} %requires eufrak
-\newcommand{\isasymbb}{\isamath{\mathfrak{b}}} %requires eufrak
-\newcommand{\isasymcc}{\isamath{\mathfrak{c}}} %requires eufrak
-\newcommand{\isasymdd}{\isamath{\mathfrak{d}}} %requires eufrak
-\newcommand{\isasymee}{\isamath{\mathfrak{e}}} %requires eufrak
-\newcommand{\isasymff}{\isamath{\mathfrak{f}}} %requires eufrak
-\newcommand{\isasymgg}{\isamath{\mathfrak{g}}} %requires eufrak
-\newcommand{\isasymhh}{\isamath{\mathfrak{h}}} %requires eufrak
-\newcommand{\isasymii}{\isamath{\mathfrak{i}}} %requires eufrak
-\newcommand{\isasymjj}{\isamath{\mathfrak{j}}} %requires eufrak
-\newcommand{\isasymkk}{\isamath{\mathfrak{k}}} %requires eufrak
-\newcommand{\isasymll}{\isamath{\mathfrak{l}}} %requires eufrak
-\newcommand{\isasymmm}{\isamath{\mathfrak{m}}} %requires eufrak
-\newcommand{\isasymnn}{\isamath{\mathfrak{n}}} %requires eufrak
-\newcommand{\isasymoo}{\isamath{\mathfrak{o}}} %requires eufrak
-\newcommand{\isasympp}{\isamath{\mathfrak{p}}} %requires eufrak
-\newcommand{\isasymqq}{\isamath{\mathfrak{q}}} %requires eufrak
-\newcommand{\isasymrr}{\isamath{\mathfrak{r}}} %requires eufrak
-\newcommand{\isasymss}{\isamath{\mathfrak{s}}} %requires eufrak
-\newcommand{\isasymtt}{\isamath{\mathfrak{t}}} %requires eufrak
-\newcommand{\isasymuu}{\isamath{\mathfrak{u}}} %requires eufrak
-\newcommand{\isasymvv}{\isamath{\mathfrak{v}}} %requires eufrak
-\newcommand{\isasymww}{\isamath{\mathfrak{w}}} %requires eufrak
-\newcommand{\isasymxx}{\isamath{\mathfrak{x}}} %requires eufrak
-\newcommand{\isasymyy}{\isamath{\mathfrak{y}}} %requires eufrak
-\newcommand{\isasymzz}{\isamath{\mathfrak{z}}} %requires eufrak
-\newcommand{\isasymalpha}{\isamath{\alpha}}
-\newcommand{\isasymbeta}{\isamath{\beta}}
-\newcommand{\isasymgamma}{\isamath{\gamma}}
-\newcommand{\isasymdelta}{\isamath{\delta}}
-\newcommand{\isasymepsilon}{\isamath{\varepsilon}}
-\newcommand{\isasymzeta}{\isamath{\zeta}}
-\newcommand{\isasymeta}{\isamath{\eta}}
-\newcommand{\isasymtheta}{\isamath{\vartheta}}
-\newcommand{\isasymiota}{\isamath{\iota}}
-\newcommand{\isasymkappa}{\isamath{\kappa}}
-\newcommand{\isasymlambda}{\isamath{\lambda}}
-\newcommand{\isasymmu}{\isamath{\mu}}
-\newcommand{\isasymnu}{\isamath{\nu}}
-\newcommand{\isasymxi}{\isamath{\xi}}
-\newcommand{\isasympi}{\isamath{\pi}}
-\newcommand{\isasymrho}{\isamath{\varrho}}
-\newcommand{\isasymsigma}{\isamath{\sigma}}
-\newcommand{\isasymtau}{\isamath{\tau}}
-\newcommand{\isasymupsilon}{\isamath{\upsilon}}
-\newcommand{\isasymphi}{\isamath{\varphi}}
-\newcommand{\isasymchi}{\isamath{\chi}}
-\newcommand{\isasympsi}{\isamath{\psi}}
-\newcommand{\isasymomega}{\isamath{\omega}}
-\newcommand{\isasymGamma}{\isamath{\Gamma}}
-\newcommand{\isasymDelta}{\isamath{\Delta}}
-\newcommand{\isasymTheta}{\isamath{\Theta}}
-\newcommand{\isasymLambda}{\isamath{\Lambda}}
-\newcommand{\isasymXi}{\isamath{\Xi}}
-\newcommand{\isasymPi}{\isamath{\Pi}}
-\newcommand{\isasymSigma}{\isamath{\Sigma}}
-\newcommand{\isasymUpsilon}{\isamath{\Upsilon}}
-\newcommand{\isasymPhi}{\isamath{\Phi}}
-\newcommand{\isasymPsi}{\isamath{\Psi}}
-\newcommand{\isasymOmega}{\isamath{\Omega}}
-\newcommand{\isasymbool}{\isamath{\mathrm{I}\mkern-3.8mu\mathrm{B}}}
-\newcommand{\isasymcomplex}{\isamath{\mathrm{C}\mkern-15mu{\phantom{\mathrm{t}}\vrule}\mkern9mu}}
-\newcommand{\isasymnat}{\isamath{\mathrm{I}\mkern-3.8mu\mathrm{N}}}
-\newcommand{\isasymrat}{\isamath{\mathrm{Q}\mkern-16mu{\phantom{\mathrm{t}}\vrule}\mkern10mu}}
-\newcommand{\isasymreal}{\isamath{\mathrm{I}\mkern-3.8mu\mathrm{R}}}
-\newcommand{\isasymint}{\isamath{\mathsf{Z}\mkern-7.5mu\mathsf{Z}}}
-\newcommand{\isasymleftarrow}{\isamath{\leftarrow}}
-\newcommand{\isasymlongleftarrow}{\isamath{\longleftarrow}}
-\newcommand{\isasymrightarrow}{\isamath{\rightarrow}}
-\newcommand{\isasymlongrightarrow}{\isamath{\longrightarrow}}
-\newcommand{\isasymLeftarrow}{\isamath{\Leftarrow}}
-\newcommand{\isasymLongleftarrow}{\isamath{\Longleftarrow}}
-\newcommand{\isasymRightarrow}{\isamath{\Rightarrow}}
-\newcommand{\isasymLongrightarrow}{\isamath{\Longrightarrow}}
-\newcommand{\isasymleftrightarrow}{\isamath{\leftrightarrow}}
-\newcommand{\isasymlongleftrightarrow}{\isamath{\longleftrightarrow}}
-\newcommand{\isasymLeftrightarrow}{\isamath{\Leftrightarrow}}
-\newcommand{\isasymLongleftrightarrow}{\isamath{\Longleftrightarrow}}
-\newcommand{\isasymmapsto}{\isamath{\mapsto}}
-\newcommand{\isasymlongmapsto}{\isamath{\longmapsto}}
-\newcommand{\isasymmidarrow}{\isamath{\relbar}}
-\newcommand{\isasymMidarrow}{\isamath{\Relbar}}
-\newcommand{\isasymhookleftarrow}{\isamath{\hookleftarrow}}
-\newcommand{\isasymhookrightarrow}{\isamath{\hookrightarrow}}
-\newcommand{\isasymleftharpoondown}{\isamath{\leftharpoondown}}
-\newcommand{\isasymrightharpoondown}{\isamath{\rightharpoondown}}
-\newcommand{\isasymleftharpoonup}{\isamath{\leftharpoonup}}
-\newcommand{\isasymrightharpoonup}{\isamath{\rightharpoonup}}
-\newcommand{\isasymrightleftharpoons}{\isamath{\rightleftharpoons}}
-\newcommand{\isasymdownharpoonleft}{\isamath{\downharpoonleft}} %requires amssymb
-\newcommand{\isasymdownharpoonright}{\isamath{\downharpoonright}} %requires amssymb
-\newcommand{\isasymupharpoonleft}{\isamath{\upharpoonleft}} %requires amssymb
-\newcommand{\isasymupharpoonright}{\isamath{\upharpoonright}} %requires amssymb
-\newcommand{\isasymrestriction}{\isamath{\restriction}} %requires amssymb
-\newcommand{\isasymleadsto}{\isamath{\leadsto}} %requires amssymb
-\newcommand{\isasymup}{\isamath{\uparrow}}
-\newcommand{\isasymUp}{\isamath{\Uparrow}}
-\newcommand{\isasymdown}{\isamath{\downarrow}}
-\newcommand{\isasymDown}{\isamath{\Downarrow}}
-\newcommand{\isasymupdown}{\isamath{\updownarrow}}
-\newcommand{\isasymUpdown}{\isamath{\Updownarrow}}
-\newcommand{\isasymlangle}{\isamath{\langle}}
-\newcommand{\isasymrangle}{\isamath{\rangle}}
-\newcommand{\isasymlceil}{\isamath{\lceil}}
-\newcommand{\isasymrceil}{\isamath{\rceil}}
-\newcommand{\isasymlfloor}{\isamath{\lfloor}}
-\newcommand{\isasymrfloor}{\isamath{\rfloor}}
-\newcommand{\isasymlparr}{\isamath{\mathopen{(\mkern-3mu\mid}}}
-\newcommand{\isasymrparr}{\isamath{\mathclose{\mid\mkern-3mu)}}}
-\newcommand{\isasymlbrakk}{\isamath{\mathopen{\lbrack\mkern-3mu\lbrack}}}
-\newcommand{\isasymrbrakk}{\isamath{\mathclose{\rbrack\mkern-3mu\rbrack}}}
-\newcommand{\isasymlbrace}{\isamath{\mathopen{\lbrace\mkern-4.5mu\mid}}}
-\newcommand{\isasymrbrace}{\isamath{\mathclose{\mid\mkern-4.5mu\rbrace}}}
-\newcommand{\isasymguillemotleft}{\isatext{\flqq}} %requires babel
-\newcommand{\isasymguillemotright}{\isatext{\frqq}} %requires babel
-\newcommand{\isasymColon}{\isamath{\mathrel{::}}}
-\newcommand{\isasymnot}{\isamath{\neg}}
-\newcommand{\isasymbottom}{\isamath{\bot}}
-\newcommand{\isasymtop}{\isamath{\top}}
-\newcommand{\isasymand}{\isamath{\wedge}}
-\newcommand{\isasymAnd}{\isamath{\bigwedge}}
-\newcommand{\isasymor}{\isamath{\vee}}
-\newcommand{\isasymOr}{\isamath{\bigvee}}
-\newcommand{\isasymforall}{\isamath{\forall\,}}
-\newcommand{\isasymexists}{\isamath{\exists\,}}
-\newcommand{\isasymbox}{\isamath{\Box}} %requires amssymb
-\newcommand{\isasymdiamond}{\isamath{\Diamond}} %requires amssymb
-\newcommand{\isasymturnstile}{\isamath{\vdash}}
-\newcommand{\isasymTurnstile}{\isamath{\models}}
-\newcommand{\isasymtturnstile}{\isamath{\vdash\!\!\!\vdash}}
-\newcommand{\isasymTTurnstile}{\isamath{\mid\!\models}}
-\newcommand{\isasymstileturn}{\isamath{\dashv}}
-\newcommand{\isasymsurd}{\isamath{\surd}}
-\newcommand{\isasymle}{\isamath{\le}}
-\newcommand{\isasymge}{\isamath{\ge}}
-\newcommand{\isasymlless}{\isamath{\ll}}
-\newcommand{\isasymggreater}{\isamath{\gg}}
-\newcommand{\isasymlesssim}{\isamath{\lesssim}} %requires amssymb
-\newcommand{\isasymgreatersim}{\isamath{\gtrsim}} %requires amssymb
-\newcommand{\isasymlessapprox}{\isamath{\lessapprox}} %requires amssymb
-\newcommand{\isasymgreaterapprox}{\isamath{\gtrapprox}} %requires amssymb
-\newcommand{\isasymin}{\isamath{\in}}
-\newcommand{\isasymnotin}{\isamath{\notin}}
-\newcommand{\isasymsubset}{\isamath{\subset}}
-\newcommand{\isasymsupset}{\isamath{\supset}}
-\newcommand{\isasymsubseteq}{\isamath{\subseteq}}
-\newcommand{\isasymsupseteq}{\isamath{\supseteq}}
-\newcommand{\isasymsqsubset}{\isamath{\sqsubset}} %requires amssymb
-\newcommand{\isasymsqsupset}{\isamath{\sqsupset}} %requires amssymb
-\newcommand{\isasymsqsubseteq}{\isamath{\sqsubseteq}}
-\newcommand{\isasymsqsupseteq}{\isamath{\sqsupseteq}}
-\newcommand{\isasyminter}{\isamath{\cap}}
-\newcommand{\isasymInter}{\isamath{\bigcap\,}}
-\newcommand{\isasymunion}{\isamath{\cup}}
-\newcommand{\isasymUnion}{\isamath{\bigcup\,}}
-\newcommand{\isasymsqunion}{\isamath{\sqcup}}
-\newcommand{\isasymSqunion}{\isamath{\bigsqcup\,}}
-\newcommand{\isasymsqinter}{\isamath{\sqcap}}
-\newcommand{\isasymSqinter}{\isamath{\bigsqcap\,}} %requires amsmath
-\newcommand{\isasymuplus}{\isamath{\uplus}}
-\newcommand{\isasymUplus}{\isamath{\biguplus\,}}
-\newcommand{\isasymnoteq}{\isamath{\not=}}
-\newcommand{\isasymsim}{\isamath{\sim}}
-\newcommand{\isasymdoteq}{\isamath{\doteq}}
-\newcommand{\isasymsimeq}{\isamath{\simeq}}
-\newcommand{\isasymapprox}{\isamath{\approx}}
-\newcommand{\isasymasymp}{\isamath{\asymp}}
-\newcommand{\isasymcong}{\isamath{\cong}}
-\newcommand{\isasymsmile}{\isamath{\smile}}
-\newcommand{\isasymequiv}{\isamath{\equiv}}
-\newcommand{\isasymfrown}{\isamath{\frown}}
-\newcommand{\isasympropto}{\isamath{\propto}}
-\newcommand{\isasymsome}{\isamath{\epsilon\,}}
-\newcommand{\isasymJoin}{\isamath{\Join}} %requires amssymb
-\newcommand{\isasymbowtie}{\isamath{\bowtie}}
-\newcommand{\isasymprec}{\isamath{\prec}}
-\newcommand{\isasymsucc}{\isamath{\succ}}
-\newcommand{\isasympreceq}{\isamath{\preceq}}
-\newcommand{\isasymsucceq}{\isamath{\succeq}}
-\newcommand{\isasymparallel}{\isamath{\parallel}}
-\newcommand{\isasymbar}{\isamath{\mid}}
-\newcommand{\isasymplusminus}{\isamath{\pm}}
-\newcommand{\isasymminusplus}{\isamath{\mp}}
-\newcommand{\isasymtimes}{\isamath{\times}}
-\newcommand{\isasymdiv}{\isamath{\div}}
-\newcommand{\isasymcdot}{\isamath{\cdot}}
-\newcommand{\isasymstar}{\isamath{\star}}
-\newcommand{\isasymbullet}{\boldmath\isamath{\mathchoice{\displaystyle{\cdot}}{\textstyle{\cdot}}{\scriptstyle{\bullet}}{\scriptscriptstyle{\bullet}}}}
-\newcommand{\isasymcirc}{\isamath{\circ}}
-\newcommand{\isasymdagger}{\isamath{\dagger}}
-\newcommand{\isasymddagger}{\isamath{\ddagger}}
-\newcommand{\isasymlhd}{\isamath{\lhd}} %requires amssymb
-\newcommand{\isasymrhd}{\isamath{\rhd}} %requires amssymb
-\newcommand{\isasymunlhd}{\isamath{\unlhd}} %requires amssymb
-\newcommand{\isasymunrhd}{\isamath{\unrhd}} %requires amssymb
-\newcommand{\isasymtriangleleft}{\isamath{\triangleleft}}
-\newcommand{\isasymtriangleright}{\isamath{\triangleright}}
-\newcommand{\isasymtriangle}{\isamath{\triangle}}
-\newcommand{\isasymtriangleq}{\isamath{\triangleq}} %requires amssymb
-\newcommand{\isasymoplus}{\isamath{\oplus}}
-\newcommand{\isasymOplus}{\isamath{\bigoplus\,}}
-\newcommand{\isasymotimes}{\isamath{\otimes}}
-\newcommand{\isasymOtimes}{\isamath{\bigotimes\,}}
-\newcommand{\isasymodot}{\isamath{\odot}}
-\newcommand{\isasymOdot}{\isamath{\bigodot\,}}
-\newcommand{\isasymominus}{\isamath{\ominus}}
-\newcommand{\isasymoslash}{\isamath{\oslash}}
-\newcommand{\isasymdots}{\isamath{\dots}}
-\newcommand{\isasymcdots}{\isamath{\cdots}}
-\newcommand{\isasymSum}{\isamath{\sum\,}}
-\newcommand{\isasymProd}{\isamath{\prod\,}}
-\newcommand{\isasymCoprod}{\isamath{\coprod\,}}
-\newcommand{\isasyminfinity}{\isamath{\infty}}
-\newcommand{\isasymintegral}{\isamath{\int\,}}
-\newcommand{\isasymointegral}{\isamath{\oint\,}}
-\newcommand{\isasymclubsuit}{\isamath{\clubsuit}}
-\newcommand{\isasymdiamondsuit}{\isamath{\diamondsuit}}
-\newcommand{\isasymheartsuit}{\isamath{\heartsuit}}
-\newcommand{\isasymspadesuit}{\isamath{\spadesuit}}
-\newcommand{\isasymaleph}{\isamath{\aleph}}
-\newcommand{\isasymemptyset}{\isamath{\emptyset}}
-\newcommand{\isasymnabla}{\isamath{\nabla}}
-\newcommand{\isasympartial}{\isamath{\partial}}
-\newcommand{\isasymRe}{\isamath{\Re}}
-\newcommand{\isasymIm}{\isamath{\Im}}
-\newcommand{\isasymflat}{\isamath{\flat}}
-\newcommand{\isasymnatural}{\isamath{\natural}}
-\newcommand{\isasymsharp}{\isamath{\sharp}}
-\newcommand{\isasymangle}{\isamath{\angle}}
-\newcommand{\isasymcopyright}{\isatext{\rm\copyright}}
-\newcommand{\isasymregistered}{\isatext{\rm\textregistered}}
-\newcommand{\isasymhyphen}{\isatext{\rm-}}
-\newcommand{\isasyminverse}{\isamath{{}^{-1}}}
-\newcommand{\isasymonesuperior}{\isamath{\mathonesuperior}} %requires latin1
-\newcommand{\isasymonequarter}{\isatext{\rm\textonequarter}} %requires latin1
-\newcommand{\isasymtwosuperior}{\isamath{\mathtwosuperior}} %requires latin1
-\newcommand{\isasymonehalf}{\isatext{\rm\textonehalf}} %requires latin1
-\newcommand{\isasymthreesuperior}{\isamath{\maththreesuperior}} %requires latin1
-\newcommand{\isasymthreequarters}{\isatext{\rm\textthreequarters}} %requires latin1
-\newcommand{\isasymordfeminine}{\isatext{\rm\textordfeminine}}
-\newcommand{\isasymordmasculine}{\isatext{\rm\textordmasculine}}
-\newcommand{\isasymsection}{\isatext{\rm\S}}
-\newcommand{\isasymparagraph}{\isatext{\rm\P}}
-\newcommand{\isasymexclamdown}{\isatext{\rm\textexclamdown}}
-\newcommand{\isasymquestiondown}{\isatext{\rm\textquestiondown}}
-\newcommand{\isasymeuro}{\isatext{\textgreek{\euro}}} %requires greek babel
-\newcommand{\isasympounds}{\isamath{\pounds}}
-\newcommand{\isasymyen}{\isatext{\yen}} %requires amssymb
-\newcommand{\isasymcent}{\isatext{\textcent}} %requires textcomp
-\newcommand{\isasymcurrency}{\isatext{\textcurrency}} %requires textcomp
-\newcommand{\isasymdegree}{\isatext{\rm\textdegree}} %requires latin1
-\newcommand{\isasymamalg}{\isamath{\amalg}}
-\newcommand{\isasymmho}{\isamath{\mho}} %requires amssymb
-\newcommand{\isasymlozenge}{\isamath{\lozenge}} %requires amssymb
-\newcommand{\isasymwp}{\isamath{\wp}}
-\newcommand{\isasymwrong}{\isamath{\wr}}
-\newcommand{\isasymstruct}{\isamath{\diamond}}
-\newcommand{\isasymacute}{\isatext{\'\relax}}
-\newcommand{\isasymindex}{\isatext{\i}}
-\newcommand{\isasymdieresis}{\isatext{\"\relax}}
-\newcommand{\isasymcedilla}{\isatext{\c\relax}}
-\newcommand{\isasymhungarumlaut}{\isatext{\H\relax}}
-\newcommand{\isasymspacespace}{\isamath{~~}}
--- a/doc-src/LaTeXsugar/Sugar/generated/mathpartir.sty Sat Apr 30 02:43:45 2005 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,354 +0,0 @@
-%%
-%% This is the original source file mathpar.sty
-%%
-%% Package `mathpar' to use with LaTeX 2e
-%% Copyright Didier Remy, all rights reserved.
-\NeedsTeXFormat{LaTeX2e}
-\ProvidesPackage{mathpartir}
- [2001/23/02 v0.92 Math Paragraph for Type Inference Rules]
-
-%%
-
-%% Identification
-%% Preliminary declarations
-
-\RequirePackage {keyval}
-
-%% Options
-%% More declarations
-
-%% PART I: Typesetting maths in paragraphe mode
-
-\newdimen \mpr@tmpdim
-
-% To ensure hevea \hva compatibility, \hva should expands to nothing
-% in mathpar or in mathrule
-\let \mpr@hva \empty
-
-%% normal paragraph parametters, should rather be taken dynamically
-\def \mpr@savepar {%
- \edef \MathparNormalpar
- {\noexpand \lineskiplimit \the\lineskiplimit
- \noexpand \lineski \the\lineskip}%
- }
-
-\def \mpr@rulelineskip {\lineskiplimit=0.3em\lineskip=0.2em plus 0.1em}
-\def \mpr@lesslineskip {\lineskiplimit=0.6em\lineskip=0.5em plus 0.2em}
-\def \mpr@lineskip {\lineskiplimit=1.2em\lineskip=1.2em plus 0.2em}
-\let \MathparLineskip \mpr@lineskip
-\def \mpr@paroptions {\MathparLineskip}
-\let \mpr@prebindings \relax
-
-\newskip \mpr@andskip \mpr@andskip 2em plus 0.5fil minus 0.5em
-
-\def \mpr@goodbreakand
- {\hskip -\mpr@andskip \penalty -1000\hskip \mpr@andskip}
-\def \mpr@and {\hskip \mpr@andskip}
-\def \mpr@andcr {\penalty 50\mpr@and}
-\def \mpr@cr {\penalty -10000\mpr@and}
-\def \mpr@eqno #1{\mpr@andcr #1\hskip 0em plus -1fil \penalty 10}
-
-\def \mpr@bindings {%
- \let \and \mpr@andcr
- \let \par \mpr@andcr
- \let \\\mpr@cr
- \let \eqno \mpr@eqno
- \let \hva \mpr@hva
- }
-\let \MathparBindings \mpr@bindings
-
-\newenvironment{mathpar}[1][]
- {$$\mpr@savepar \parskip 0em \hsize \linewidth \centering
- \vbox \bgroup \mpr@prebindings \mpr@paroptions #1\ifmmode $\else
- \noindent $\displaystyle\fi
- \MathparBindings}
- {\unskip \ifmmode $\fi\egroup $$\ignorespacesafterend}
-
-% \def \math@mathpar #1{\setbox0 \hbox {$\displaystyle #1$}\ifnum
-% \wd0 < \hsize $$\box0$$\else \bmathpar #1\emathpar \fi}
-
-%%% HOV BOXES
-
-\def \mathvbox@ #1{\hbox \bgroup \mpr@normallineskip
- \vbox \bgroup \tabskip 0em \let \\ \cr
- \halign \bgroup \hfil $##$\hfil\cr #1\crcr \egroup \egroup
- \egroup}
-
-\def \mathhvbox@ #1{\setbox0 \hbox {\let \\\qquad $#1$}\ifnum \wd0 < \hsize
- \box0\else \mathvbox {#1}\fi}
-
-
-%% Part II -- operations on lists
-
-\newtoks \mpr@lista
-\newtoks \mpr@listb
-
-\long \def\mpr@cons #1\to#2{\mpr@lista {\\{#1}}\mpr@listb \expandafter
-{#2}\edef #2{\the \mpr@lista \the \mpr@listb}}
-
-\long \def\mpr@snoc #1\to#2{\mpr@lista {\\{#1}}\mpr@listb \expandafter
-{#2}\edef #2{\the \mpr@listb\the\mpr@lista}}
-
-\long \def \mpr@concat#1=#2\to#3{\mpr@lista \expandafter {#2}\mpr@listb
-\expandafter {#3}\edef #1{\the \mpr@listb\the\mpr@lista}}
-
-\def \mpr@head #1\to #2{\expandafter \mpr@head@ #1\mpr@head@ #1#2}
-\long \def \mpr@head@ #1#2\mpr@head@ #3#4{\def #4{#1}\def#3{#2}}
-
-\def \mpr@flatten #1\to #2{\expandafter \mpr@flatten@ #1\mpr@flatten@ #1#2}
-\long \def \mpr@flatten@ \\#1\\#2\mpr@flatten@ #3#4{\def #4{#1}\def #3{\\#2}}
-
-\def \mpr@makelist #1\to #2{\def \mpr@all {#1}%
- \mpr@lista {\\}\mpr@listb \expandafter {\mpr@all}\edef \mpr@all {\the
- \mpr@lista \the \mpr@listb \the \mpr@lista}\let #2\empty
- \def \mpr@stripof ##1##2\mpr@stripend{\def \mpr@stripped{##2}}\loop
- \mpr@flatten \mpr@all \to \mpr@one
- \expandafter \mpr@snoc \mpr@one \to #2\expandafter \mpr@stripof
- \mpr@all \mpr@stripend
- \ifx \mpr@stripped \empty \let \mpr@isempty 0\else \let \mpr@isempty 1\fi
- \ifx 1\mpr@isempty
- \repeat
-}
-
-%% Part III -- Type inference rules
-
-\def \mpr@rev #1\to #2{\let \mpr@tmp \empty
- \def \\##1{\mpr@cons ##1\to \mpr@tmp}#1\let #2\mpr@tmp}
-
-\newif \if@premisse
-\newbox \mpr@hlist
-\newbox \mpr@vlist
-\newif \ifmpr@center \mpr@centertrue
-\def \mpr@htovlist {%
- \setbox \mpr@hlist
- \hbox {\strut
- \ifmpr@center \hskip -0.5\wd\mpr@hlist\fi
- \unhbox \mpr@hlist}%
- \setbox \mpr@vlist
- \vbox {\if@premisse \box \mpr@hlist \unvbox \mpr@vlist
- \else \unvbox \mpr@vlist \box \mpr@hlist
- \fi}%
-}
-% OLD version
-% \def \mpr@htovlist {%
-% \setbox \mpr@hlist
-% \hbox {\strut \hskip -0.5\wd\mpr@hlist \unhbox \mpr@hlist}%
-% \setbox \mpr@vlist
-% \vbox {\if@premisse \box \mpr@hlist \unvbox \mpr@vlist
-% \else \unvbox \mpr@vlist \box \mpr@hlist
-% \fi}%
-% }
-
-
-
-
-\def \mpr@blank { }
-\def \mpr@hovbox #1#2{\hbox
- \bgroup
- \ifx #1T\@premissetrue
- \else \ifx #1B\@premissefalse
- \else
- \PackageError{mathpartir}
- {Premisse orientation should either be P or B}
- {Fatal error in Package}%
- \fi \fi
- \def \@test {#2}\ifx \@test \mpr@blank\else
- \setbox \mpr@hlist \hbox {}%
- \setbox \mpr@vlist \vbox {}%
- \if@premisse \let \snoc \mpr@cons \else \let \snoc \mpr@snoc \fi
- \let \@hvlist \empty \let \@rev \empty
- \mpr@tmpdim 0em
- \expandafter \mpr@makelist #2\to \mpr@flat
- \if@premisse \mpr@rev \mpr@flat \to \@rev \else \let \@rev \mpr@flat \fi
- \def \\##1{%
- \def \@test {##1}\ifx \@test \empty
- \mpr@htovlist
- \mpr@tmpdim 0em %%% last bug fix not extensively checked
- \else
- \setbox0 \hbox{$\displaystyle {##1}$}\relax
- \advance \mpr@tmpdim by \wd0
- %\mpr@tmpdim 1.02\mpr@tmpdim
- \ifnum \mpr@tmpdim < \hsize
- \ifnum \wd\mpr@hlist > 0
- \if@premisse
- \setbox \mpr@hlist \hbox {\unhbox0 \qquad \unhbox \mpr@hlist}%
- \else
- \setbox \mpr@hlist \hbox {\unhbox \mpr@hlist \qquad \unhbox0}%
- \fi
- \else
- \setbox \mpr@hlist \hbox {\unhbox0}%
- \fi
- \else
- \ifnum \wd \mpr@hlist > 0
- \mpr@htovlist
- \mpr@tmpdim \wd0
- \fi
- \setbox \mpr@hlist \hbox {\unhbox0}%
- \fi
- \advance \mpr@tmpdim by 2em
- \fi
- }%
- \@rev
- \mpr@htovlist
- \ifmpr@center \hskip \wd\mpr@vlist\fi \box \mpr@vlist
- \fi
- \egroup
-}
-
-%%% INFERENCE RULES
-
-\@ifundefined{@@over}{%
- \let\@@over\over % fallback if amsmath is not loaded
- \let\@@overwithdelims\overwithdelims
- \let\@@atop\atop \let\@@atopwithdelims\atopwithdelims
- \let\@@above\above \let\@@abovewithdelims\abovewithdelims
- }{}
-
-
-\def \mpr@@fraction #1#2{\hbox {\advance \hsize by -0.5em
- $\displaystyle {#1\@@over #2}$}}
-\let \mpr@fraction \mpr@@fraction
-\def \mpr@@reduce #1#2{\hbox
- {$\lower 0.01pt \mpr@@fraction {#1}{#2}\mkern -15mu\rightarrow$}}
-\def \mpr@infercenter #1{\vcenter {\mpr@hovbox{T}{#1}}}
-
-\def \mpr@empty {}
-\def \mpr@inferrule
- {\bgroup
- \mpr@rulelineskip
- \let \and \qquad
- \let \hva \mpr@hva
- \let \@rulename \mpr@empty
- \let \@rule@options \mpr@empty
- \mpr@inferrule@}
-\newcommand {\mpr@inferrule@}[3][]
- {\everymath={\displaystyle}%
- \def \@test {#2}\ifx \empty \@test
- \setbox0 \hbox {$\vcenter {\mpr@hovbox{B}{#3}}$}%
- \else
- \def \@test {#3}\ifx \empty \@test
- \setbox0 \hbox {$\vcenter {\mpr@hovbox{T}{#2}}$}%
- \else
- \setbox0 \mpr@fraction {\mpr@hovbox{T}{#2}}{\mpr@hovbox{B}{#3}}%
- \fi \fi
- \def \@test {#1}\ifx \@test\empty \box0
- \else \vbox
-%%% Suggestion de Francois pour les etiquettes longues
-%%% {\hbox to \wd0 {\TirName {#1}\hfil}\box0}\fi
- {\hbox {\TirName {#1}}\box0}\fi
- \egroup}
-
-\def \mpr@vdotfil #1{\vbox to #1{\leaders \hbox{$\cdot$} \vfil}}
-
-% They are two forms
-% \mathrule [label]{[premisses}{conclusions}
-% or
-% \mathrule* [options]{[premisses}{conclusions}
-%
-% Premisses and conclusions are lists of elements separated by \\
-% Each \\ produces a break, attempting horizontal breaks if possible,
-% and vertical breaks if needed.
-%
-% An empty element obtained by \\\\ produces a vertical break in all cases.
-%
-% The former rule is aligned on the fraction bar.
-% The optional label appears on top of the rule
-% The second form to be used in a derivation tree is aligned on the last
-% line of its conclusion
-%
-% The second form can be parameterized, using the key=val interface. The
-% folloiwng keys are recognized:
-%
-% width set the width of the rule to val
-% narrower set the width of the rule to val\hsize
-% before execute val at the beginning/left
-% lab put a label [Val] on top of the rule
-% lskip add negative skip on the right
-% llab put a left label [Val], ignoring its width
-% left put a left label [Val]
-% right put a right label [Val]
-% rlab put a right label [Val], ignoring its width
-% rskip add negative skip on the left
-% vdots lift the rule by val and fill vertical space with dots
-% after execute val at the end/right
-%
-% Note that most options must come in this order to avoid strange
-% typesetting (in particular lskip must preceed left and llab and
-% rskip must follow rlab or right; vdots must come last or be followed by
-% rskip.
-%
-
-\define@key {mprset}{flushleft}[]{\mpr@centerfalse}
-\define@key {mprset}{center}[]{\mpr@centertrue}
-\def \mprset #1{\setkeys{mprset}{#1}}
-
-\newbox \mpr@right
-\define@key {mpr}{flushleft}[]{\mpr@centerfalse}
-\define@key {mpr}{center}[]{\mpr@centertrue}
-\define@key {mpr}{left}{\setbox0 \hbox {$\TirName {#1}\;$}\relax
- \advance \hsize by -\wd0\box0}
-\define@key {mpr}{width}{\hsize #1}
-\define@key {mpr}{before}{#1}
-\define@key {mpr}{lab}{\def \mpr@rulename {[#1]}}
-\define@key {mpr}{Lab}{\def \mpr@rulename {#1}}
-\define@key {mpr}{narrower}{\hsize #1\hsize}
-\define@key {mpr}{leftskip}{\hskip -#1}
-\define@key {mpr}{reduce}[]{\let \mpr@fraction \mpr@@reduce}
-\define@key {mpr}{rightskip}
- {\setbox \mpr@right \hbox {\unhbox \mpr@right \hskip -#1}}
-\define@key {mpr}{left}{\setbox0 \hbox {$\TirName {#1}\;$}\relax
- \advance \hsize by -\wd0\box0}
-\define@key {mpr}{Left}{\llap{$\TirName {#1}\;$}}
-\define@key {mpr}{right}
- {\setbox0 \hbox {$\;\TirName {#1}$}\relax \advance \hsize by -\wd0
- \setbox \mpr@right \hbox {\unhbox \mpr@right \unhbox0}}
-\define@key {mpr}{Right}
- {\setbox \mpr@right \hbox {\unhbox \mpr@right \rlap {$\;\TirName {#1}$}}}
-\define@key {mpr}{vdots}{\def \mpr@vdots {\@@atop \mpr@vdotfil{#1}}}
-\define@key {mpr}{after}{\edef \mpr@after {\mpr@after #1}}
-
-\newdimen \rule@dimen
-\newcommand \mpr@inferstar@ [3][]{\setbox0
- \hbox {\let \mpr@rulename \mpr@empty \let \mpr@vdots \relax
- \setbox \mpr@right \hbox{}%
- $\setkeys{mpr}{#1}%
- \ifx \mpr@rulename \mpr@empty \mpr@inferrule {#2}{#3}\else
- \mpr@inferrule [{\mpr@rulename}]{#2}{#3}\fi
- \box \mpr@right \mpr@vdots$}
- \setbox1 \hbox {\strut}
- \rule@dimen \dp0 \advance \rule@dimen by -\dp1
- \raise \rule@dimen \box0}
-
-\def \mpr@infer {\@ifnextchar *{\mpr@inferstar}{\mpr@inferrule}}
-\newcommand \mpr@err@skipargs[3][]{}
-\def \mpr@inferstar*{\ifmmode
- \let \@do \mpr@inferstar@
- \else
- \let \@do \mpr@err@skipargs
- \PackageError {mathpartir}
- {\string\inferrule* can only be used in math mode}{}%
- \fi \@do}
-
-
-%%% Exports
-
-% Envirnonment mathpar
-
-\let \inferrule \mpr@infer
-
-% make a short name \infer is not already defined
-\@ifundefined {infer}{\let \infer \mpr@infer}{}
-
-\def \tir@name #1{\hbox {\small \sc #1}}
-\let \TirName \tir@name
-
-%%% Other Exports
-
-% \let \listcons \mpr@cons
-% \let \listsnoc \mpr@snoc
-% \let \listhead \mpr@head
-% \let \listmake \mpr@makelist
-
-
-\endinput
-
--- a/doc-src/LaTeXsugar/Sugar/generated/pdfsetup.sty Sat Apr 30 02:43:45 2005 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,11 +0,0 @@
-%%
-%% Author: Markus Wenzel, TU Muenchen
-%%
-%% smart url or hyperref setup
-%%
-
-\@ifundefined{pdfoutput}
-{\usepackage{url}}
-{\usepackage{color}\definecolor{darkblue}{rgb}{0,0,0.5}
- \usepackage[pdftex,a4paper,colorlinks=true,linkcolor=darkblue,citecolor=darkblue,filecolor=darkblue,pagecolor=darkblue,urlcolor=darkblue]{hyperref}
- \IfFileExists{thumbpdf.sty}{\usepackage{thumbpdf}}{}}
--- a/doc-src/LaTeXsugar/Sugar/generated/root.bib Sat Apr 30 02:43:45 2005 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,12 +0,0 @@
-@book{LNCS2283,author={Tobias Nipkow and Lawrence Paulson and Markus Wenzel},
-title="Isabelle/HOL --- A Proof Assistant for Higher-Order Logic",
-publisher=Springer,series=LNCS,volume=2283,year=2002,
-note={\url{http://www.in.tum.de/~nipkow/LNCS2283/}}}
-
-@misc{mathpartir,author={Didier R\'emy},title={mathpartir},
-note={\url{http://cristal.inria.fr/~remy/latex/}}}
-
-@misc{tar,author={Gerwin Klein and Norber Schirmer and Tobias Nipkow},
-title={{LaTeX} sugar theories and support files},
-note={\url{http://isabelle.in.tum.de/sugar.tar.gz}}}
-
--- a/doc-src/LaTeXsugar/Sugar/generated/root.tex Sat Apr 30 02:43:45 2005 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,59 +0,0 @@
-\documentclass[11pt,a4paper]{article}
-\usepackage{isabelle,isabellesym}
-
-% further packages required for unusual symbols (see also isabellesym.sty)
-% use only when needed
-%\usepackage{amssymb} % for \<leadsto>, \<box>, \<diamond>,
- % \<sqsupset>, \<mho>, \<Join>,
- % \<lhd>, \<lesssim>, \<greatersim>,
- % \<lessapprox>, \<greaterapprox>,
- % \<triangleq>, \<yen>, \<lozenge>
-%\usepackage[greek,english]{babel} % greek for \<euro>,
- % english for \<guillemotleft>,
- % \<guillemotright>
- % default language = last
-%\usepackage[latin1]{inputenc} % for \<onesuperior>, \<onequarter>,
- % \<twosuperior>, \<onehalf>,
- % \<threesuperior>, \<threequarters>,
- % \<degree>
-%\usepackage[only,bigsqcap]{stmaryrd} % for \<Sqinter>
-%\usepackage{eufrak} % for \<AA> ... \<ZZ>, \<aa> ... \<zz>
- % (only needed if amssymb not used)
-%\usepackage{textcomp} % for \<cent>, \<currency>
-
-\usepackage{mathpartir}
-
-% this should be the last package used
-\usepackage{pdfsetup}
-
-% urls in roman style, theory text in math-similar italics
-\urlstyle{rm}
-\isabellestyle{it}
-
-\hyphenation{Isa-belle}
-\begin{document}
-
-\title{\LaTeX\ Sugar for Isabelle documents}
-\author{Gerwin Klein, Tobias Nipkow, Norbert Schirmer}
-\maketitle
-
-\begin{abstract}
-This document shows how to typset mathematics in Isabelle-based
-documents in a style close to that in ordinary computer science papers.
-\end{abstract}
-
-\tableofcontents
-
-% generated text of all theories
-\input{Sugar.tex}
-
-% optional bibliography
-\bibliographystyle{abbrv}
-\bibliography{root}
-
-\end{document}
-
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: t
-%%% End:
--- a/doc-src/LaTeXsugar/Sugar/generated/session.tex Sat Apr 30 02:43:45 2005 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,10 +0,0 @@
-\input{LaTeXsugar.tex}
-
-\input{OptionalSugar.tex}
-
-\input{Sugar.tex}
-
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: "root"
-%%% End: