# HG changeset patch # User kleing # Date 1114821917 -7200 # Node ID 41f9c0902db1dafe35d430da0a7ee7ed18bab0ce # Parent c0cd613a49eb9e262d06d865aa00110246cb8053 move generated files to document/ to avoid CVS file overwrite in generated/ cleanup (no generated root.pdf, session_graph.pdf etc) diff -r c0cd613a49eb -r 41f9c0902db1 doc-src/LaTeXsugar/IsaMakefile --- 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 diff -r c0cd613a49eb -r 41f9c0902db1 doc-src/LaTeXsugar/Makefile --- 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 diff -r c0cd613a49eb -r 41f9c0902db1 doc-src/LaTeXsugar/Sugar/generated/LaTeXsugar.tex diff -r c0cd613a49eb -r 41f9c0902db1 doc-src/LaTeXsugar/Sugar/generated/OptionalSugar.tex diff -r c0cd613a49eb -r 41f9c0902db1 doc-src/LaTeXsugar/Sugar/generated/Sugar.tex --- 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: diff -r c0cd613a49eb -r 41f9c0902db1 doc-src/LaTeXsugar/Sugar/generated/isabelle.sty --- 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}% -} diff -r c0cd613a49eb -r 41f9c0902db1 doc-src/LaTeXsugar/Sugar/generated/isabellesym.sty --- 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{~~}} diff -r c0cd613a49eb -r 41f9c0902db1 doc-src/LaTeXsugar/Sugar/generated/mathpartir.sty --- 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 - diff -r c0cd613a49eb -r 41f9c0902db1 doc-src/LaTeXsugar/Sugar/generated/pdfsetup.sty --- 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}}{}} diff -r c0cd613a49eb -r 41f9c0902db1 doc-src/LaTeXsugar/Sugar/generated/root.bib --- 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}}} - diff -r c0cd613a49eb -r 41f9c0902db1 doc-src/LaTeXsugar/Sugar/generated/root.tex --- 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 \, \, \, - % \, \, \, - % \, \, \, - % \, \, - % \, \, \ -%\usepackage[greek,english]{babel} % greek for \, - % english for \, - % \ - % default language = last -%\usepackage[latin1]{inputenc} % for \, \, - % \, \, - % \, \, - % \ -%\usepackage[only,bigsqcap]{stmaryrd} % for \ -%\usepackage{eufrak} % for \ ... \, \ ... \ - % (only needed if amssymb not used) -%\usepackage{textcomp} % for \, \ - -\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: diff -r c0cd613a49eb -r 41f9c0902db1 doc-src/LaTeXsugar/Sugar/generated/session.tex --- 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: