1.1 --- a/doc-src/LaTeXsugar/IsaMakefile Sat Apr 30 02:43:45 2005 +0200
1.2 +++ b/doc-src/LaTeXsugar/IsaMakefile Sat Apr 30 02:45:17 2005 +0200
1.3 @@ -14,7 +14,7 @@
1.4 OUT = $(ISABELLE_OUTPUT)
1.5 LOG = $(OUT)/log
1.6
1.7 -USEDIR = $(ISATOOL) usedir -v true -i true -d pdf -D generated -H false
1.8 +USEDIR = $(ISATOOL) usedir -v true -i false -g false -d false -D document -H false
1.9
1.10
1.11 ## Sugar
2.1 --- a/doc-src/LaTeXsugar/Makefile Sat Apr 30 02:43:45 2005 +0200
2.2 +++ b/doc-src/LaTeXsugar/Makefile Sat Apr 30 02:45:17 2005 +0200
2.3 @@ -8,7 +8,7 @@
2.4
2.5 ## paths
2.6
2.7 -SRCPATH = Sugar/generated
2.8 +SRCPATH = Sugar/document
2.9
2.10 ## dependencies
2.11
2.12 @@ -16,31 +16,31 @@
2.13
2.14 NAME = sugar
2.15
2.16 -FILES = Sugar/generated/root.tex Sugar/generated/root.bib \
2.17 - Sugar/generated/mathpartir.sty Sugar/generated/LaTeXsugar.tex \
2.18 - Sugar/generated/OptionalSugar.tex
2.19 +FILES = Sugar/document/root.tex Sugar/document/root.bib \
2.20 + Sugar/document/mathpartir.sty Sugar/document/LaTeXsugar.tex \
2.21 + Sugar/document/OptionalSugar.tex
2.22
2.23 -GARBAGE = Sugar/generated/*.aux Sugar/generated/*.log Sugar/generated/*.toc \
2.24 - Sugar/generated/*.idx Sugar/generated/*.bbl Sugar/generated/*.blg \
2.25 - Sugar/generated/*.out
2.26 +GARBAGE = Sugar/document/*.aux Sugar/document/*.log Sugar/document/*.toc \
2.27 + Sugar/document/*.idx Sugar/document/*.bbl Sugar/document/*.blg \
2.28 + Sugar/document/*.out
2.29
2.30 dvi: $(NAME).dvi
2.31
2.32 $(NAME).dvi: $(FILES)
2.33 - cd Sugar/generated; \
2.34 + cd Sugar/document; \
2.35 $(LATEX) root; \
2.36 $(BIBTEX) root; \
2.37 $(LATEX) root; \
2.38 $(LATEX) root
2.39 - cp $(SRCPATH)/root.dvi $(NAME).dvi
2.40 + mv $(SRCPATH)/root.dvi $(NAME).dvi
2.41
2.42 pdf: $(NAME).pdf
2.43
2.44 $(NAME).pdf: $(FILES)
2.45 - cd Sugar/generated; \
2.46 + cd Sugar/document; \
2.47 $(PDFLATEX) root; \
2.48 $(BIBTEX) root; \
2.49 $(PDFLATEX) root; \
2.50 $(PDFLATEX) root
2.51 - cp $(SRCPATH)/root.pdf $(NAME).pdf
2.52 + mv $(SRCPATH)/root.pdf $(NAME).pdf
2.53
3.1 --- a/doc-src/LaTeXsugar/Sugar/generated/Sugar.tex Sat Apr 30 02:43:45 2005 +0200
3.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
3.3 @@ -1,363 +0,0 @@
3.4 -%
3.5 -\begin{isabellebody}%
3.6 -\def\isabellecontext{Sugar}%
3.7 -\isamarkupfalse%
3.8 -%
3.9 -\isamarkupsection{Introduction%
3.10 -}
3.11 -\isamarkuptrue%
3.12 -%
3.13 -\begin{isamarkuptext}%
3.14 -This document is for those Isabelle users who have mastered
3.15 -the art of mixing \LaTeX\ text and Isabelle theories and never want to
3.16 -typeset a theorem by hand anymore because they have experienced the
3.17 -bliss of writing \verb!@!\verb!{thm[display]setsum_cartesian_product[no_vars]}!
3.18 -and seeing Isabelle typeset it for them:
3.19 -\begin{isabelle}%
3.20 -{\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}%
3.21 -\end{isabelle}
3.22 -No typos, no omissions, no sweat.
3.23 -If you have not experienced that joy, read Chapter 4, \emph{Presenting
3.24 -Theories}, \cite{LNCS2283} first.
3.25 -
3.26 -If you have mastered the art of Isabelle's \emph{antiquotations},
3.27 -i.e.\ things like the above \verb!@!\verb!{thm...}!, beware: in your vanity
3.28 -you may be tempted to think that all readers of the stunning ps or pdf
3.29 -documents you can now produce at the drop of a hat will be struck with
3.30 -awe at the beauty unfolding in front of their eyes. Until one day you
3.31 -come across that very critical of readers known as the ``common referee''.
3.32 -He has the nasty habit of refusing to understand unfamiliar notation
3.33 -like Isabelle's infamous \isa{{\isasymlbrakk}\ {\isasymrbrakk}\ {\isasymLongrightarrow}} no matter how many times you
3.34 -explain it in your paper. Even worse, he thinks that using \isa{{\isasymlbrakk}\ {\isasymrbrakk}} for anything other than denotational semantics is a cardinal sin
3.35 -that must be punished by instant rejection.
3.36 -
3.37 -
3.38 -This document shows you how to make Isabelle and \LaTeX\ cooperate to
3.39 -produce ordinary looking mathematics that hides the fact that it was
3.40 -typeset by a machine. You merely need to load the right files:
3.41 -\begin{itemize}
3.42 -\item Import theory \texttt{LaTeXsugar} in the header of your own
3.43 -theory. You may also want bits of \texttt{OptionalSugar}, which you can
3.44 -copy selectively into your own theory or import as a whole. Both
3.45 -theories live in \texttt{HOL/Library} and are found automatically.
3.46 -
3.47 -\item Should you need additional \LaTeX\ packages (the text will tell
3.48 -you so), you include them at the beginning of your \LaTeX\ document,
3.49 -typically in \texttt{root.tex}.
3.50 -\end{itemize}%
3.51 -\end{isamarkuptext}%
3.52 -\isamarkuptrue%
3.53 -%
3.54 -\isamarkupsection{HOL syntax%
3.55 -}
3.56 -\isamarkuptrue%
3.57 -%
3.58 -\isamarkupsubsection{Logic%
3.59 -}
3.60 -\isamarkuptrue%
3.61 -%
3.62 -\begin{isamarkuptext}%
3.63 -The predefined constructs \isa{if}, \isa{let} and
3.64 -\isa{case} are set in sans serif font to distinguish them from
3.65 -other functions. This improves readability:
3.66 -\begin{itemize}
3.67 -\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}}}.
3.68 -\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}}}.
3.69 -\item \isa{\textsf{case}\ x\ \textsf{of}\ True\ {\isasymRightarrow}\ e\isactrlisub {\isadigit{1}}\ {\isacharbar}\ False\ {\isasymRightarrow}\ e\isactrlisub {\isadigit{2}}} instead of\\
3.70 - \isa{case\ x\ of\ True\ {\isasymRightarrow}\ e\isactrlisub {\isadigit{1}}\ {\isacharbar}\ False\ {\isasymRightarrow}\ e\isactrlisub {\isadigit{2}}}.
3.71 -\end{itemize}%
3.72 -\end{isamarkuptext}%
3.73 -\isamarkuptrue%
3.74 -%
3.75 -\isamarkupsubsection{Sets%
3.76 -}
3.77 -\isamarkuptrue%
3.78 -%
3.79 -\begin{isamarkuptext}%
3.80 -Although set syntax in HOL is already close to
3.81 -standard, we provide a few further improvements:
3.82 -\begin{itemize}
3.83 -\item \isa{{\isacharbraceleft}x\ {\isacharbar}\ P{\isacharbraceright}} instead of \isa{{\isacharbraceleft}x{\isachardot}\ P{\isacharbraceright}}.
3.84 -\item \isa{{\isasymemptyset}} instead of \isa{{\isacharbraceleft}{\isacharbraceright}}.
3.85 -\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}}.
3.86 -\end{itemize}%
3.87 -\end{isamarkuptext}%
3.88 -\isamarkuptrue%
3.89 -%
3.90 -\isamarkupsubsection{Lists%
3.91 -}
3.92 -\isamarkuptrue%
3.93 -%
3.94 -\begin{isamarkuptext}%
3.95 -If lists are used heavily, the following notations increase readability:
3.96 -\begin{itemize}
3.97 -\item \isa{x{\isasymcdot}xs} instead of \isa{x\ {\isacharhash}\ xs}.
3.98 - Exceptionally, \isa{x{\isasymcdot}xs} is also input syntax.
3.99 -If you prefer more space around the $\cdot$ you have to redefine
3.100 -\verb!\isasymcdot! in \LaTeX:
3.101 -\verb!\renewcommand{\isasymcdot}{\isamath{\,\cdot\,}}!
3.102 -
3.103 -\item \isa{{\isacharbar}xs{\isacharbar}} instead of \isa{length\ xs}.
3.104 -\item \isa{xs\ensuremath{_{[\mathit{n}]}}} instead of \isa{nth\ xs\ n},
3.105 - the $n$th element of \isa{xs}.
3.106 -
3.107 -\item The \isa{{\isacharat}} operation associates implicitly to the right,
3.108 -which leads to unpleasant line breaks if the term is too long for one
3.109 -line. To avoid this, \texttt{OptionalSugar} contains syntax to group
3.110 -\isa{{\isacharat}}-terms to the left before printing, which leads to better
3.111 -line breaking behaviour:
3.112 -\begin{isabelle}%
3.113 -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}}%
3.114 -\end{isabelle}
3.115 -
3.116 -\end{itemize}%
3.117 -\end{isamarkuptext}%
3.118 -\isamarkuptrue%
3.119 -%
3.120 -\isamarkupsection{Printing theorems%
3.121 -}
3.122 -\isamarkuptrue%
3.123 -%
3.124 -\isamarkupsubsection{Question marks%
3.125 -}
3.126 -\isamarkuptrue%
3.127 -%
3.128 -\begin{isamarkuptext}%
3.129 -If you print anything, especially theorems, containing
3.130 -schematic variables they are prefixed with a question mark:
3.131 -\verb!@!\verb!{thm conjI}! results in \isa{{\isasymlbrakk}{\isacharquery}P{\isacharsemicolon}\ {\isacharquery}Q{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}P\ {\isasymand}\ {\isacharquery}Q}. Most of the time
3.132 -you would rather not see the question marks. There is an attribute
3.133 -\verb!no_vars! that you can attach to the theorem that turns its
3.134 -schematic into ordinary free variables: \verb!@!\verb!{thm conjI[no_vars]}!
3.135 -results in \isa{{\isasymlbrakk}P{\isacharsemicolon}\ Q{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ {\isasymand}\ Q}.
3.136 -
3.137 -This \verb!no_vars! business can become a bit tedious.
3.138 -If you would rather never see question marks, simply put
3.139 -\begin{verbatim}
3.140 -reset show_var_qmarks;
3.141 -\end{verbatim}
3.142 -at the beginning of your file \texttt{ROOT.ML}.
3.143 -The rest of this document is produced with this flag reset.%
3.144 -\end{isamarkuptext}%
3.145 -\isamarkuptrue%
3.146 -\isamarkupfalse%
3.147 -%
3.148 -\isamarkupsubsection{Inference rules%
3.149 -}
3.150 -\isamarkuptrue%
3.151 -%
3.152 -\begin{isamarkuptext}%
3.153 -To print theorems as inference rules you need to include Didier
3.154 -R\'emy's \texttt{mathpartir} package~\cite{mathpartir}
3.155 -for typesetting inference rules in your \LaTeX\ file.
3.156 -
3.157 -Writing \verb!@!\verb!{thm[mode=Rule] conjI}! produces
3.158 -\isa{\mbox{}\inferrule{\mbox{P}\\\ \mbox{Q}}{\mbox{P\ {\isasymand}\ Q}}}, even in the middle of a sentence.
3.159 -If you prefer your inference rule on a separate line, maybe with a name,
3.160 -\begin{center}
3.161 -\isa{\mbox{}\inferrule{\mbox{P}\\\ \mbox{Q}}{\mbox{P\ {\isasymand}\ Q}}} {\sc conjI}
3.162 -\end{center}
3.163 -is produced by
3.164 -\begin{quote}
3.165 -\verb!\begin{center}!\\
3.166 -\verb!@!\verb!{thm[mode=Rule] conjI} {\sc conjI}!\\
3.167 -\verb!\end{center}!
3.168 -\end{quote}
3.169 -It is not recommended to use the standard \texttt{display} attribute
3.170 -together with \texttt{Rule} because centering does not work and because
3.171 -the line breaking mechanisms of \texttt{display} and \texttt{mathpartir} can
3.172 -clash.
3.173 -
3.174 -Of course you can display multiple rules in this fashion:
3.175 -\begin{quote}
3.176 -\verb!\begin{center}\isastyle!\\
3.177 -\verb!@!\verb!{thm[mode=Rule] conjI} {\sc conjI} \\[1ex]!\\
3.178 -\verb!@!\verb!{thm[mode=Rule] conjE} {\sc disjI$_1$} \qquad!\\
3.179 -\verb!@!\verb!{thm[mode=Rule] disjE} {\sc disjI$_2$}!\\
3.180 -\verb!\end{center}!
3.181 -\end{quote}
3.182 -yields
3.183 -\begin{center}\isastyle
3.184 -\isa{\mbox{}\inferrule{\mbox{P}\\\ \mbox{Q}}{\mbox{P\ {\isasymand}\ Q}}} {\sc conjI} \\[1ex]
3.185 -\isa{\mbox{}\inferrule{\mbox{P}}{\mbox{P\ {\isasymor}\ Q}}} {\sc disjI$_1$} \qquad
3.186 -\isa{\mbox{}\inferrule{\mbox{Q}}{\mbox{P\ {\isasymor}\ Q}}} {\sc disjI$_2$}
3.187 -\end{center}
3.188 -Note that we included \verb!\isastyle! to obtain
3.189 -the smaller font that otherwise comes only with \texttt{display}.
3.190 -
3.191 -The \texttt{mathpartir} package copes well if there are too many
3.192 -premises for one line:
3.193 -\begin{center}
3.194 -\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}}}
3.195 -\end{center}
3.196 -
3.197 -Limitations: 1. Premises and conclusion must each not be longer than
3.198 -the line. 2. Premises that are \isa{{\isasymLongrightarrow}}-implications are again
3.199 -displayed with a horizontal line, which looks at least unusual.%
3.200 -\end{isamarkuptext}%
3.201 -\isamarkuptrue%
3.202 -%
3.203 -\isamarkupsubsection{If-then%
3.204 -}
3.205 -\isamarkuptrue%
3.206 -%
3.207 -\begin{isamarkuptext}%
3.208 -If you prefer a fake ``natural language'' style you can produce
3.209 -the body of
3.210 -\newtheorem{theorem}{Theorem}
3.211 -\begin{theorem}
3.212 -\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}}
3.213 -\end{theorem}
3.214 -by typing
3.215 -\begin{quote}
3.216 -\verb!@!\verb!{thm[mode=IfThen] le_trans}!
3.217 -\end{quote}
3.218 -
3.219 -In order to prevent odd line breaks, the premises are put into boxes.
3.220 -At times this is too drastic:
3.221 -\begin{theorem}
3.222 -\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}}
3.223 -\end{theorem}
3.224 -In which case you should use \texttt{mode=IfThenNoBox} instead of
3.225 -\texttt{mode=IfThen}:
3.226 -\begin{theorem}
3.227 -\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}}
3.228 -\end{theorem}%
3.229 -\end{isamarkuptext}%
3.230 -\isamarkuptrue%
3.231 -%
3.232 -\isamarkupsubsection{Definitions and Equations%
3.233 -}
3.234 -\isamarkuptrue%
3.235 -%
3.236 -\begin{isamarkuptext}%
3.237 -The \verb!thm! antiquotation works nicely for proper theorems, but
3.238 - sets of equations as used in definitions are more difficult to
3.239 - typeset nicely: for some reason people tend to prefer aligned
3.240 - \isa{{\isacharequal}} signs.
3.241 -
3.242 - Isabelle2005 has a nice mechanism for this, namely the two
3.243 - antiquotations \verb!@!\verb!{lhs thm}! and \verb!@!\verb!{rhs thm}!.
3.244 -
3.245 - \begin{center}
3.246 - \begin{tabular}{l@ {~~\isa{{\isacharequal}}~~}l}
3.247 - \isa{foldl\ f\ a\ {\isacharbrackleft}{\isacharbrackright}} & \isa{a}\\
3.248 - \isa{foldl\ f\ a\ {\isacharparenleft}x{\isasymcdot}xs{\isacharparenright}} & \isa{foldl\ f\ {\isacharparenleft}f\ a\ x{\isacharparenright}\ xs}
3.249 - \end{tabular}
3.250 - \end{center}
3.251 -
3.252 - \noindent
3.253 - is produced by the following code:
3.254 -
3.255 -\begin{quote}
3.256 - \verb!\begin{center}!\\
3.257 - \verb!\begin{tabular}{l@ {~~!\verb!@!\verb!{text "="}~~}l}!\\
3.258 - \verb!@!\verb!{lhs foldl_Nil} & @!\verb!{rhs foldl_Nil}!\\
3.259 - \verb!@!\verb!{lhs foldl_Cons} & @!\verb!{rhs foldl_Cons}!\\
3.260 - \verb!\end{tabular}!\\
3.261 - \verb!\end{center}!
3.262 -\end{quote}
3.263 -
3.264 - \noindent
3.265 - Note the space between \verb!@! and \verb!{! in the tabular argument.
3.266 - It prevents Isabelle from interpreting \verb!@ {~~...~~}!
3.267 - as antiquotation. \verb!@!\verb!{lhs thm}! and \verb!@!\verb!{rhs thm}!
3.268 - try to be smart about the interpretation of the theorem they
3.269 - print, they work just as well for meta equality \isa{{\isasymequiv}} and other
3.270 - binary operators like \isa{{\isacharless}}.%
3.271 -\end{isamarkuptext}%
3.272 -\isamarkuptrue%
3.273 -%
3.274 -\isamarkupsubsection{Patterns%
3.275 -}
3.276 -\isamarkuptrue%
3.277 -%
3.278 -\begin{isamarkuptext}%
3.279 -Sometimes functions ignore one or more of their
3.280 - arguments and some functional languages have nice
3.281 - syntax for that as in \isa{hd\ {\isacharparenleft}x{\isasymcdot}\_{\isacharparenright}\ {\isacharequal}\ x}.
3.282 -
3.283 - You can simulate this in Isabelle by instantiating the \isa{xs} in
3.284 - definition \mbox{\isa{hd\ {\isacharparenleft}x{\isasymcdot}xs{\isacharparenright}\ {\isacharequal}\ x}} with a constant \isa{DUMMY} that
3.285 - is printed as \isa{\_}. The code for the pattern above is
3.286 - \verb!@!\verb!{thm hd.simps [where xs=DUMMY]}!.
3.287 -
3.288 - You can drive this game even further and extend the syntax of let
3.289 - bindings such that certain functions like \isa{fst}, \isa{hd},
3.290 - etc.\ are printed as patterns. \texttt{OptionalSugar} provides the
3.291 - following:
3.292 -
3.293 - \begin{center}
3.294 - \begin{tabular}{l@ {~~produced by~~}l}
3.295 - \isa{\textsf{let}\ {\isacharparenleft}x{\isacharcomma}\ \_{\isacharparenright}\ {\isacharequal}\ p\ \textsf{in}\ t} & \verb!@!\verb!{term "let x = fst p in t"}!\\
3.296 - \isa{\textsf{let}\ {\isacharparenleft}\_{\isacharcomma}\ x{\isacharparenright}\ {\isacharequal}\ p\ \textsf{in}\ t} & \verb!@!\verb!{term "let x = snd p in t"}!\\
3.297 - \isa{\textsf{let}\ x{\isasymcdot}\_\ {\isacharequal}\ xs\ \textsf{in}\ t} & \verb!@!\verb!{term "let x = hd xs in t"}!\\
3.298 - \isa{\textsf{let}\ \_{\isasymcdot}x\ {\isacharequal}\ xs\ \textsf{in}\ t} & \verb!@!\verb!{term "let x = tl xs in t"}!\\
3.299 - \isa{\textsf{let}\ Some\ x\ {\isacharequal}\ y\ \textsf{in}\ t} & \verb!@!\verb!{term "let x = the y in t"}!\\
3.300 - \end{tabular}
3.301 - \end{center}%
3.302 -\end{isamarkuptext}%
3.303 -\isamarkuptrue%
3.304 -%
3.305 -\isamarkupsubsection{Proofs%
3.306 -}
3.307 -\isamarkuptrue%
3.308 -%
3.309 -\begin{isamarkuptext}%
3.310 -Full proofs, even if written in beautiful Isar style, are likely to
3.311 - be too long and detailed to be included in conference papers, but
3.312 - some key lemmas might be of interest.
3.313 -
3.314 - It is usually easiest to put them in figures like the one in Fig.\
3.315 - \ref{fig:proof}. This was achieved with the \isakeyword{text\_raw}
3.316 - command:%
3.317 -\end{isamarkuptext}%
3.318 -\isamarkuptrue%
3.319 -%
3.320 -\begin{figure}
3.321 - \begin{center}\begin{minipage}{0.6\textwidth}
3.322 - \isastyle\isamarkuptrue
3.323 -\isacommand{lemma}\ True\isanewline
3.324 -\isamarkupfalse%
3.325 -\isacommand{proof}\ {\isacharminus}\isanewline
3.326 -\ \ %
3.327 -\isamarkupcmt{pretty trivial%
3.328 -}
3.329 -\isanewline
3.330 -\ \ \isamarkupfalse%
3.331 -\isacommand{show}\ True\ \isamarkupfalse%
3.332 -\isacommand{by}\ force\isanewline
3.333 -\isamarkupfalse%
3.334 -\isacommand{qed}\isamarkupfalse%
3.335 -%
3.336 -\end{minipage}\end{center}
3.337 - \caption{Example proof in a figure.}\label{fig:proof}
3.338 - \end{figure}
3.339 -%
3.340 -\begin{isamarkuptext}%
3.341 -\begin{quote}
3.342 -\small
3.343 -\verb!text_raw {!\verb!*!\\
3.344 -\verb! \begin{figure}!\\
3.345 -\verb! \begin{center}\begin{minipage}{0.6\textwidth}!\\
3.346 -\verb! \isastyle\isamarkuptrue!\\
3.347 -\verb!*!\verb!}!\\
3.348 -\verb!lemma True!\\
3.349 -\verb!proof -!\\
3.350 -\verb! -- "pretty trivial"!\\
3.351 -\verb! show True by force!\\
3.352 -\verb!qed!\\
3.353 -\verb!text_raw {!\verb!*!\\
3.354 -\verb! \end{minipage}\end{center}!\\
3.355 -\verb! \caption{Example proof in a figure.}\label{fig:proof}!\\
3.356 -\verb! \end{figure}!\\
3.357 -\verb!*!\verb!}!
3.358 -\end{quote}%
3.359 -\end{isamarkuptext}%
3.360 -\isamarkuptrue%
3.361 -\isamarkupfalse%
3.362 -\end{isabellebody}%
3.363 -%%% Local Variables:
3.364 -%%% mode: latex
3.365 -%%% TeX-master: "root"
3.366 -%%% End:
4.1 --- a/doc-src/LaTeXsugar/Sugar/generated/isabelle.sty Sat Apr 30 02:43:45 2005 +0200
4.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
4.3 @@ -1,164 +0,0 @@
4.4 -%%
4.5 -%% Author: Markus Wenzel, TU Muenchen
4.6 -%%
4.7 -%% macros for Isabelle generated LaTeX output
4.8 -%%
4.9 -
4.10 -%%% Simple document preparation (based on theory token language and symbols)
4.11 -
4.12 -% isabelle environments
4.13 -
4.14 -\newcommand{\isabellecontext}{UNKNOWN}
4.15 -
4.16 -\newcommand{\isastyle}{\small\tt\slshape}
4.17 -\newcommand{\isastyleminor}{\small\tt\slshape}
4.18 -\newcommand{\isastylescript}{\footnotesize\tt\slshape}
4.19 -\newcommand{\isastyletext}{\normalsize\rm}
4.20 -\newcommand{\isastyletxt}{\rm}
4.21 -\newcommand{\isastylecmt}{\rm}
4.22 -
4.23 -%symbol markup -- \emph achieves decent spacing via italic corrections
4.24 -\newcommand{\isamath}[1]{\emph{$#1$}}
4.25 -\newcommand{\isatext}[1]{\emph{#1}}
4.26 -\newcommand{\isascriptstyle}{\def\isamath##1{##1}\def\isatext##1{\mbox{\isastylescript##1}}}
4.27 -\newcommand{\isactrlsub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
4.28 -\newcommand{\isactrlsup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
4.29 -\newcommand{\isactrlisub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
4.30 -\newcommand{\isactrlisup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
4.31 -\newcommand{\isactrlbsub}{\emph\bgroup\begin{math}{}\sb\bgroup\mbox\bgroup\isastylescript}
4.32 -\newcommand{\isactrlesub}{\egroup\egroup\end{math}\egroup}
4.33 -\newcommand{\isactrlbsup}{\emph\bgroup\begin{math}{}\sp\bgroup\mbox\bgroup\isastylescript}
4.34 -\newcommand{\isactrlesup}{\egroup\egroup\end{math}\egroup}
4.35 -\newcommand{\isactrlbold}[1]{{\bfseries\upshape\boldmath#1}}
4.36 -
4.37 -
4.38 -\newdimen\isa@parindent\newdimen\isa@parskip
4.39 -
4.40 -\newenvironment{isabellebody}{%
4.41 -\isamarkuptrue\par%
4.42 -\isa@parindent\parindent\parindent0pt%
4.43 -\isa@parskip\parskip\parskip0pt%
4.44 -\isastyle}{\par}
4.45 -
4.46 -\newenvironment{isabelle}
4.47 -{\begin{trivlist}\begin{isabellebody}\item\relax}
4.48 -{\end{isabellebody}\end{trivlist}}
4.49 -
4.50 -\newcommand{\isa}[1]{\emph{\isastyleminor #1}}
4.51 -
4.52 -\newcommand{\isaindent}[1]{\hphantom{#1}}
4.53 -\newcommand{\isanewline}{\mbox{}\par\mbox{}}
4.54 -\newcommand{\isasep}{} % override with e.g. \renewcommand{\isasep}{\vspace{1ex}}
4.55 -\newcommand{\isadigit}[1]{#1}
4.56 -
4.57 -\chardef\isacharbang=`\!
4.58 -\chardef\isachardoublequote=`\"
4.59 -\chardef\isacharhash=`\#
4.60 -\chardef\isachardollar=`\$
4.61 -\chardef\isacharpercent=`\%
4.62 -\chardef\isacharampersand=`\&
4.63 -\chardef\isacharprime=`\'
4.64 -\chardef\isacharparenleft=`\(
4.65 -\chardef\isacharparenright=`\)
4.66 -\chardef\isacharasterisk=`\*
4.67 -\chardef\isacharplus=`\+
4.68 -\chardef\isacharcomma=`\,
4.69 -\chardef\isacharminus=`\-
4.70 -\chardef\isachardot=`\.
4.71 -\chardef\isacharslash=`\/
4.72 -\chardef\isacharcolon=`\:
4.73 -\chardef\isacharsemicolon=`\;
4.74 -\chardef\isacharless=`\<
4.75 -\chardef\isacharequal=`\=
4.76 -\chardef\isachargreater=`\>
4.77 -\chardef\isacharquery=`\?
4.78 -\chardef\isacharat=`\@
4.79 -\chardef\isacharbrackleft=`\[
4.80 -\chardef\isacharbackslash=`\\
4.81 -\chardef\isacharbrackright=`\]
4.82 -\chardef\isacharcircum=`\^
4.83 -\chardef\isacharunderscore=`\_
4.84 -\chardef\isacharbackquote=`\`
4.85 -\chardef\isacharbraceleft=`\{
4.86 -\chardef\isacharbar=`\|
4.87 -\chardef\isacharbraceright=`\}
4.88 -\chardef\isachartilde=`\~
4.89 -
4.90 -
4.91 -% keyword and section markup
4.92 -
4.93 -\newcommand{\isakeywordcharunderscore}{\_}
4.94 -\newcommand{\isakeyword}[1]
4.95 -{\emph{\bf\def\isachardot{.}\def\isacharunderscore{\isakeywordcharunderscore}%
4.96 -\def\isacharbraceleft{\{}\def\isacharbraceright{\}}#1}}
4.97 -\newcommand{\isacommand}[1]{\isakeyword{#1}}
4.98 -
4.99 -\newcommand{\isamarkupheader}[1]{\section{#1}}
4.100 -\newcommand{\isamarkupchapter}[1]{\chapter{#1}}
4.101 -\newcommand{\isamarkupsection}[1]{\section{#1}}
4.102 -\newcommand{\isamarkupsubsection}[1]{\subsection{#1}}
4.103 -\newcommand{\isamarkupsubsubsection}[1]{\subsubsection{#1}}
4.104 -\newcommand{\isamarkupsect}[1]{\section{#1}}
4.105 -\newcommand{\isamarkupsubsect}[1]{\subsection{#1}}
4.106 -\newcommand{\isamarkupsubsubsect}[1]{\subsubsection{#1}}
4.107 -
4.108 -\newif\ifisamarkup
4.109 -\newcommand{\isabeginpar}{\par\ifisamarkup\relax\else\medskip\fi}
4.110 -\newcommand{\isaendpar}{\par\medskip}
4.111 -\newenvironment{isapar}{\parindent\isa@parindent\parskip\isa@parskip\isabeginpar}{\isaendpar}
4.112 -\newenvironment{isamarkuptext}{\isastyletext\begin{isapar}}{\end{isapar}}
4.113 -\newenvironment{isamarkuptxt}{\isastyletxt\begin{isapar}}{\end{isapar}}
4.114 -\newcommand{\isamarkupcmt}[1]{{\isastylecmt--- #1}}
4.115 -
4.116 -
4.117 -% alternative styles
4.118 -
4.119 -\newcommand{\isabellestyle}{}
4.120 -\def\isabellestyle#1{\csname isabellestyle#1\endcsname}
4.121 -
4.122 -\newcommand{\isabellestylett}{%
4.123 -\renewcommand{\isastyle}{\small\tt}%
4.124 -\renewcommand{\isastyleminor}{\small\tt}%
4.125 -\renewcommand{\isastylescript}{\footnotesize\tt}%
4.126 -}
4.127 -\newcommand{\isabellestyleit}{%
4.128 -\renewcommand{\isastyle}{\small\it}%
4.129 -\renewcommand{\isastyleminor}{\it}%
4.130 -\renewcommand{\isastylescript}{\footnotesize\it}%
4.131 -\renewcommand{\isakeywordcharunderscore}{\mbox{-}}%
4.132 -\renewcommand{\isacharbang}{\isamath{!}}%
4.133 -\renewcommand{\isachardoublequote}{}%
4.134 -\renewcommand{\isacharhash}{\isamath{\#}}%
4.135 -\renewcommand{\isachardollar}{\isamath{\$}}%
4.136 -\renewcommand{\isacharpercent}{\isamath{\%}}%
4.137 -\renewcommand{\isacharampersand}{\isamath{\&}}%
4.138 -\renewcommand{\isacharprime}{\isamath{\mskip2mu{'}\mskip-2mu}}%
4.139 -\renewcommand{\isacharparenleft}{\isamath{(}}%
4.140 -\renewcommand{\isacharparenright}{\isamath{)}}%
4.141 -\renewcommand{\isacharasterisk}{\isamath{*}}%
4.142 -\renewcommand{\isacharplus}{\isamath{+}}%
4.143 -\renewcommand{\isacharcomma}{\isamath{\mathord,}}%
4.144 -\renewcommand{\isacharminus}{\isamath{-}}%
4.145 -\renewcommand{\isachardot}{\isamath{\mathord.}}%
4.146 -\renewcommand{\isacharslash}{\isamath{/}}%
4.147 -\renewcommand{\isacharcolon}{\isamath{\mathord:}}%
4.148 -\renewcommand{\isacharsemicolon}{\isamath{\mathord;}}%
4.149 -\renewcommand{\isacharless}{\isamath{<}}%
4.150 -\renewcommand{\isacharequal}{\isamath{=}}%
4.151 -\renewcommand{\isachargreater}{\isamath{>}}%
4.152 -\renewcommand{\isacharat}{\isamath{@}}%
4.153 -\renewcommand{\isacharbrackleft}{\isamath{[}}%
4.154 -\renewcommand{\isacharbrackright}{\isamath{]}}%
4.155 -\renewcommand{\isacharunderscore}{\mbox{-}}%
4.156 -\renewcommand{\isacharbraceleft}{\isamath{\{}}%
4.157 -\renewcommand{\isacharbar}{\isamath{\mid}}%
4.158 -\renewcommand{\isacharbraceright}{\isamath{\}}}%
4.159 -\renewcommand{\isachartilde}{\isamath{{}\sp{\sim}}}%
4.160 -}
4.161 -
4.162 -\newcommand{\isabellestylesl}{%
4.163 -\isabellestyleit%
4.164 -\renewcommand{\isastyle}{\small\sl}%
4.165 -\renewcommand{\isastyleminor}{\sl}%
4.166 -\renewcommand{\isastylescript}{\footnotesize\sl}%
4.167 -}
5.1 --- a/doc-src/LaTeXsugar/Sugar/generated/isabellesym.sty Sat Apr 30 02:43:45 2005 +0200
5.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
5.3 @@ -1,359 +0,0 @@
5.4 -%%
5.5 -%% Author: Markus Wenzel, TU Muenchen
5.6 -%%
5.7 -%% definitions of standard Isabelle symbols
5.8 -%%
5.9 -
5.10 -% symbol definitions
5.11 -
5.12 -\newcommand{\isasymzero}{\isamath{\mathbf{0}}} %requires amssymb
5.13 -\newcommand{\isasymone}{\isamath{\mathbf{1}}} %requires amssymb
5.14 -\newcommand{\isasymtwo}{\isamath{\mathbf{2}}} %requires amssymb
5.15 -\newcommand{\isasymthree}{\isamath{\mathbf{3}}} %requires amssymb
5.16 -\newcommand{\isasymfour}{\isamath{\mathbf{4}}} %requires amssymb
5.17 -\newcommand{\isasymfive}{\isamath{\mathbf{5}}} %requires amssymb
5.18 -\newcommand{\isasymsix}{\isamath{\mathbf{6}}} %requires amssymb
5.19 -\newcommand{\isasymseven}{\isamath{\mathbf{7}}} %requires amssymb
5.20 -\newcommand{\isasymeight}{\isamath{\mathbf{8}}} %requires amssymb
5.21 -\newcommand{\isasymnine}{\isamath{\mathbf{9}}} %requires amssymb
5.22 -\newcommand{\isasymA}{\isamath{\mathcal{A}}}
5.23 -\newcommand{\isasymB}{\isamath{\mathcal{B}}}
5.24 -\newcommand{\isasymC}{\isamath{\mathcal{C}}}
5.25 -\newcommand{\isasymD}{\isamath{\mathcal{D}}}
5.26 -\newcommand{\isasymE}{\isamath{\mathcal{E}}}
5.27 -\newcommand{\isasymF}{\isamath{\mathcal{F}}}
5.28 -\newcommand{\isasymG}{\isamath{\mathcal{G}}}
5.29 -\newcommand{\isasymH}{\isamath{\mathcal{H}}}
5.30 -\newcommand{\isasymI}{\isamath{\mathcal{I}}}
5.31 -\newcommand{\isasymJ}{\isamath{\mathcal{J}}}
5.32 -\newcommand{\isasymK}{\isamath{\mathcal{K}}}
5.33 -\newcommand{\isasymL}{\isamath{\mathcal{L}}}
5.34 -\newcommand{\isasymM}{\isamath{\mathcal{M}}}
5.35 -\newcommand{\isasymN}{\isamath{\mathcal{N}}}
5.36 -\newcommand{\isasymO}{\isamath{\mathcal{O}}}
5.37 -\newcommand{\isasymP}{\isamath{\mathcal{P}}}
5.38 -\newcommand{\isasymQ}{\isamath{\mathcal{Q}}}
5.39 -\newcommand{\isasymR}{\isamath{\mathcal{R}}}
5.40 -\newcommand{\isasymS}{\isamath{\mathcal{S}}}
5.41 -\newcommand{\isasymT}{\isamath{\mathcal{T}}}
5.42 -\newcommand{\isasymU}{\isamath{\mathcal{U}}}
5.43 -\newcommand{\isasymV}{\isamath{\mathcal{V}}}
5.44 -\newcommand{\isasymW}{\isamath{\mathcal{W}}}
5.45 -\newcommand{\isasymX}{\isamath{\mathcal{X}}}
5.46 -\newcommand{\isasymY}{\isamath{\mathcal{Y}}}
5.47 -\newcommand{\isasymZ}{\isamath{\mathcal{Z}}}
5.48 -\newcommand{\isasyma}{\isamath{\mathrm{a}}}
5.49 -\newcommand{\isasymb}{\isamath{\mathrm{b}}}
5.50 -\newcommand{\isasymc}{\isamath{\mathrm{c}}}
5.51 -\newcommand{\isasymd}{\isamath{\mathrm{d}}}
5.52 -\newcommand{\isasyme}{\isamath{\mathrm{e}}}
5.53 -\newcommand{\isasymf}{\isamath{\mathrm{f}}}
5.54 -\newcommand{\isasymg}{\isamath{\mathrm{g}}}
5.55 -\newcommand{\isasymh}{\isamath{\mathrm{h}}}
5.56 -\newcommand{\isasymi}{\isamath{\mathrm{i}}}
5.57 -\newcommand{\isasymj}{\isamath{\mathrm{j}}}
5.58 -\newcommand{\isasymk}{\isamath{\mathrm{k}}}
5.59 -\newcommand{\isasyml}{\isamath{\mathrm{l}}}
5.60 -\newcommand{\isasymm}{\isamath{\mathrm{m}}}
5.61 -\newcommand{\isasymn}{\isamath{\mathrm{n}}}
5.62 -\newcommand{\isasymo}{\isamath{\mathrm{o}}}
5.63 -\newcommand{\isasymp}{\isamath{\mathrm{p}}}
5.64 -\newcommand{\isasymq}{\isamath{\mathrm{q}}}
5.65 -\newcommand{\isasymr}{\isamath{\mathrm{r}}}
5.66 -\newcommand{\isasyms}{\isamath{\mathrm{s}}}
5.67 -\newcommand{\isasymt}{\isamath{\mathrm{t}}}
5.68 -\newcommand{\isasymu}{\isamath{\mathrm{u}}}
5.69 -\newcommand{\isasymv}{\isamath{\mathrm{v}}}
5.70 -\newcommand{\isasymw}{\isamath{\mathrm{w}}}
5.71 -\newcommand{\isasymx}{\isamath{\mathrm{x}}}
5.72 -\newcommand{\isasymy}{\isamath{\mathrm{y}}}
5.73 -\newcommand{\isasymz}{\isamath{\mathrm{z}}}
5.74 -\newcommand{\isasymAA}{\isamath{\mathfrak{A}}} %requires eufrak
5.75 -\newcommand{\isasymBB}{\isamath{\mathfrak{B}}} %requires eufrak
5.76 -\newcommand{\isasymCC}{\isamath{\mathfrak{C}}} %requires eufrak
5.77 -\newcommand{\isasymDD}{\isamath{\mathfrak{D}}} %requires eufrak
5.78 -\newcommand{\isasymEE}{\isamath{\mathfrak{E}}} %requires eufrak
5.79 -\newcommand{\isasymFF}{\isamath{\mathfrak{F}}} %requires eufrak
5.80 -\newcommand{\isasymGG}{\isamath{\mathfrak{G}}} %requires eufrak
5.81 -\newcommand{\isasymHH}{\isamath{\mathfrak{H}}} %requires eufrak
5.82 -\newcommand{\isasymII}{\isamath{\mathfrak{I}}} %requires eufrak
5.83 -\newcommand{\isasymJJ}{\isamath{\mathfrak{J}}} %requires eufrak
5.84 -\newcommand{\isasymKK}{\isamath{\mathfrak{K}}} %requires eufrak
5.85 -\newcommand{\isasymLL}{\isamath{\mathfrak{L}}} %requires eufrak
5.86 -\newcommand{\isasymMM}{\isamath{\mathfrak{M}}} %requires eufrak
5.87 -\newcommand{\isasymNN}{\isamath{\mathfrak{N}}} %requires eufrak
5.88 -\newcommand{\isasymOO}{\isamath{\mathfrak{O}}} %requires eufrak
5.89 -\newcommand{\isasymPP}{\isamath{\mathfrak{P}}} %requires eufrak
5.90 -\newcommand{\isasymQQ}{\isamath{\mathfrak{Q}}} %requires eufrak
5.91 -\newcommand{\isasymRR}{\isamath{\mathfrak{R}}} %requires eufrak
5.92 -\newcommand{\isasymSS}{\isamath{\mathfrak{S}}} %requires eufrak
5.93 -\newcommand{\isasymTT}{\isamath{\mathfrak{T}}} %requires eufrak
5.94 -\newcommand{\isasymUU}{\isamath{\mathfrak{U}}} %requires eufrak
5.95 -\newcommand{\isasymVV}{\isamath{\mathfrak{V}}} %requires eufrak
5.96 -\newcommand{\isasymWW}{\isamath{\mathfrak{W}}} %requires eufrak
5.97 -\newcommand{\isasymXX}{\isamath{\mathfrak{X}}} %requires eufrak
5.98 -\newcommand{\isasymYY}{\isamath{\mathfrak{Y}}} %requires eufrak
5.99 -\newcommand{\isasymZZ}{\isamath{\mathfrak{Z}}} %requires eufrak
5.100 -\newcommand{\isasymaa}{\isamath{\mathfrak{a}}} %requires eufrak
5.101 -\newcommand{\isasymbb}{\isamath{\mathfrak{b}}} %requires eufrak
5.102 -\newcommand{\isasymcc}{\isamath{\mathfrak{c}}} %requires eufrak
5.103 -\newcommand{\isasymdd}{\isamath{\mathfrak{d}}} %requires eufrak
5.104 -\newcommand{\isasymee}{\isamath{\mathfrak{e}}} %requires eufrak
5.105 -\newcommand{\isasymff}{\isamath{\mathfrak{f}}} %requires eufrak
5.106 -\newcommand{\isasymgg}{\isamath{\mathfrak{g}}} %requires eufrak
5.107 -\newcommand{\isasymhh}{\isamath{\mathfrak{h}}} %requires eufrak
5.108 -\newcommand{\isasymii}{\isamath{\mathfrak{i}}} %requires eufrak
5.109 -\newcommand{\isasymjj}{\isamath{\mathfrak{j}}} %requires eufrak
5.110 -\newcommand{\isasymkk}{\isamath{\mathfrak{k}}} %requires eufrak
5.111 -\newcommand{\isasymll}{\isamath{\mathfrak{l}}} %requires eufrak
5.112 -\newcommand{\isasymmm}{\isamath{\mathfrak{m}}} %requires eufrak
5.113 -\newcommand{\isasymnn}{\isamath{\mathfrak{n}}} %requires eufrak
5.114 -\newcommand{\isasymoo}{\isamath{\mathfrak{o}}} %requires eufrak
5.115 -\newcommand{\isasympp}{\isamath{\mathfrak{p}}} %requires eufrak
5.116 -\newcommand{\isasymqq}{\isamath{\mathfrak{q}}} %requires eufrak
5.117 -\newcommand{\isasymrr}{\isamath{\mathfrak{r}}} %requires eufrak
5.118 -\newcommand{\isasymss}{\isamath{\mathfrak{s}}} %requires eufrak
5.119 -\newcommand{\isasymtt}{\isamath{\mathfrak{t}}} %requires eufrak
5.120 -\newcommand{\isasymuu}{\isamath{\mathfrak{u}}} %requires eufrak
5.121 -\newcommand{\isasymvv}{\isamath{\mathfrak{v}}} %requires eufrak
5.122 -\newcommand{\isasymww}{\isamath{\mathfrak{w}}} %requires eufrak
5.123 -\newcommand{\isasymxx}{\isamath{\mathfrak{x}}} %requires eufrak
5.124 -\newcommand{\isasymyy}{\isamath{\mathfrak{y}}} %requires eufrak
5.125 -\newcommand{\isasymzz}{\isamath{\mathfrak{z}}} %requires eufrak
5.126 -\newcommand{\isasymalpha}{\isamath{\alpha}}
5.127 -\newcommand{\isasymbeta}{\isamath{\beta}}
5.128 -\newcommand{\isasymgamma}{\isamath{\gamma}}
5.129 -\newcommand{\isasymdelta}{\isamath{\delta}}
5.130 -\newcommand{\isasymepsilon}{\isamath{\varepsilon}}
5.131 -\newcommand{\isasymzeta}{\isamath{\zeta}}
5.132 -\newcommand{\isasymeta}{\isamath{\eta}}
5.133 -\newcommand{\isasymtheta}{\isamath{\vartheta}}
5.134 -\newcommand{\isasymiota}{\isamath{\iota}}
5.135 -\newcommand{\isasymkappa}{\isamath{\kappa}}
5.136 -\newcommand{\isasymlambda}{\isamath{\lambda}}
5.137 -\newcommand{\isasymmu}{\isamath{\mu}}
5.138 -\newcommand{\isasymnu}{\isamath{\nu}}
5.139 -\newcommand{\isasymxi}{\isamath{\xi}}
5.140 -\newcommand{\isasympi}{\isamath{\pi}}
5.141 -\newcommand{\isasymrho}{\isamath{\varrho}}
5.142 -\newcommand{\isasymsigma}{\isamath{\sigma}}
5.143 -\newcommand{\isasymtau}{\isamath{\tau}}
5.144 -\newcommand{\isasymupsilon}{\isamath{\upsilon}}
5.145 -\newcommand{\isasymphi}{\isamath{\varphi}}
5.146 -\newcommand{\isasymchi}{\isamath{\chi}}
5.147 -\newcommand{\isasympsi}{\isamath{\psi}}
5.148 -\newcommand{\isasymomega}{\isamath{\omega}}
5.149 -\newcommand{\isasymGamma}{\isamath{\Gamma}}
5.150 -\newcommand{\isasymDelta}{\isamath{\Delta}}
5.151 -\newcommand{\isasymTheta}{\isamath{\Theta}}
5.152 -\newcommand{\isasymLambda}{\isamath{\Lambda}}
5.153 -\newcommand{\isasymXi}{\isamath{\Xi}}
5.154 -\newcommand{\isasymPi}{\isamath{\Pi}}
5.155 -\newcommand{\isasymSigma}{\isamath{\Sigma}}
5.156 -\newcommand{\isasymUpsilon}{\isamath{\Upsilon}}
5.157 -\newcommand{\isasymPhi}{\isamath{\Phi}}
5.158 -\newcommand{\isasymPsi}{\isamath{\Psi}}
5.159 -\newcommand{\isasymOmega}{\isamath{\Omega}}
5.160 -\newcommand{\isasymbool}{\isamath{\mathrm{I}\mkern-3.8mu\mathrm{B}}}
5.161 -\newcommand{\isasymcomplex}{\isamath{\mathrm{C}\mkern-15mu{\phantom{\mathrm{t}}\vrule}\mkern9mu}}
5.162 -\newcommand{\isasymnat}{\isamath{\mathrm{I}\mkern-3.8mu\mathrm{N}}}
5.163 -\newcommand{\isasymrat}{\isamath{\mathrm{Q}\mkern-16mu{\phantom{\mathrm{t}}\vrule}\mkern10mu}}
5.164 -\newcommand{\isasymreal}{\isamath{\mathrm{I}\mkern-3.8mu\mathrm{R}}}
5.165 -\newcommand{\isasymint}{\isamath{\mathsf{Z}\mkern-7.5mu\mathsf{Z}}}
5.166 -\newcommand{\isasymleftarrow}{\isamath{\leftarrow}}
5.167 -\newcommand{\isasymlongleftarrow}{\isamath{\longleftarrow}}
5.168 -\newcommand{\isasymrightarrow}{\isamath{\rightarrow}}
5.169 -\newcommand{\isasymlongrightarrow}{\isamath{\longrightarrow}}
5.170 -\newcommand{\isasymLeftarrow}{\isamath{\Leftarrow}}
5.171 -\newcommand{\isasymLongleftarrow}{\isamath{\Longleftarrow}}
5.172 -\newcommand{\isasymRightarrow}{\isamath{\Rightarrow}}
5.173 -\newcommand{\isasymLongrightarrow}{\isamath{\Longrightarrow}}
5.174 -\newcommand{\isasymleftrightarrow}{\isamath{\leftrightarrow}}
5.175 -\newcommand{\isasymlongleftrightarrow}{\isamath{\longleftrightarrow}}
5.176 -\newcommand{\isasymLeftrightarrow}{\isamath{\Leftrightarrow}}
5.177 -\newcommand{\isasymLongleftrightarrow}{\isamath{\Longleftrightarrow}}
5.178 -\newcommand{\isasymmapsto}{\isamath{\mapsto}}
5.179 -\newcommand{\isasymlongmapsto}{\isamath{\longmapsto}}
5.180 -\newcommand{\isasymmidarrow}{\isamath{\relbar}}
5.181 -\newcommand{\isasymMidarrow}{\isamath{\Relbar}}
5.182 -\newcommand{\isasymhookleftarrow}{\isamath{\hookleftarrow}}
5.183 -\newcommand{\isasymhookrightarrow}{\isamath{\hookrightarrow}}
5.184 -\newcommand{\isasymleftharpoondown}{\isamath{\leftharpoondown}}
5.185 -\newcommand{\isasymrightharpoondown}{\isamath{\rightharpoondown}}
5.186 -\newcommand{\isasymleftharpoonup}{\isamath{\leftharpoonup}}
5.187 -\newcommand{\isasymrightharpoonup}{\isamath{\rightharpoonup}}
5.188 -\newcommand{\isasymrightleftharpoons}{\isamath{\rightleftharpoons}}
5.189 -\newcommand{\isasymdownharpoonleft}{\isamath{\downharpoonleft}} %requires amssymb
5.190 -\newcommand{\isasymdownharpoonright}{\isamath{\downharpoonright}} %requires amssymb
5.191 -\newcommand{\isasymupharpoonleft}{\isamath{\upharpoonleft}} %requires amssymb
5.192 -\newcommand{\isasymupharpoonright}{\isamath{\upharpoonright}} %requires amssymb
5.193 -\newcommand{\isasymrestriction}{\isamath{\restriction}} %requires amssymb
5.194 -\newcommand{\isasymleadsto}{\isamath{\leadsto}} %requires amssymb
5.195 -\newcommand{\isasymup}{\isamath{\uparrow}}
5.196 -\newcommand{\isasymUp}{\isamath{\Uparrow}}
5.197 -\newcommand{\isasymdown}{\isamath{\downarrow}}
5.198 -\newcommand{\isasymDown}{\isamath{\Downarrow}}
5.199 -\newcommand{\isasymupdown}{\isamath{\updownarrow}}
5.200 -\newcommand{\isasymUpdown}{\isamath{\Updownarrow}}
5.201 -\newcommand{\isasymlangle}{\isamath{\langle}}
5.202 -\newcommand{\isasymrangle}{\isamath{\rangle}}
5.203 -\newcommand{\isasymlceil}{\isamath{\lceil}}
5.204 -\newcommand{\isasymrceil}{\isamath{\rceil}}
5.205 -\newcommand{\isasymlfloor}{\isamath{\lfloor}}
5.206 -\newcommand{\isasymrfloor}{\isamath{\rfloor}}
5.207 -\newcommand{\isasymlparr}{\isamath{\mathopen{(\mkern-3mu\mid}}}
5.208 -\newcommand{\isasymrparr}{\isamath{\mathclose{\mid\mkern-3mu)}}}
5.209 -\newcommand{\isasymlbrakk}{\isamath{\mathopen{\lbrack\mkern-3mu\lbrack}}}
5.210 -\newcommand{\isasymrbrakk}{\isamath{\mathclose{\rbrack\mkern-3mu\rbrack}}}
5.211 -\newcommand{\isasymlbrace}{\isamath{\mathopen{\lbrace\mkern-4.5mu\mid}}}
5.212 -\newcommand{\isasymrbrace}{\isamath{\mathclose{\mid\mkern-4.5mu\rbrace}}}
5.213 -\newcommand{\isasymguillemotleft}{\isatext{\flqq}} %requires babel
5.214 -\newcommand{\isasymguillemotright}{\isatext{\frqq}} %requires babel
5.215 -\newcommand{\isasymColon}{\isamath{\mathrel{::}}}
5.216 -\newcommand{\isasymnot}{\isamath{\neg}}
5.217 -\newcommand{\isasymbottom}{\isamath{\bot}}
5.218 -\newcommand{\isasymtop}{\isamath{\top}}
5.219 -\newcommand{\isasymand}{\isamath{\wedge}}
5.220 -\newcommand{\isasymAnd}{\isamath{\bigwedge}}
5.221 -\newcommand{\isasymor}{\isamath{\vee}}
5.222 -\newcommand{\isasymOr}{\isamath{\bigvee}}
5.223 -\newcommand{\isasymforall}{\isamath{\forall\,}}
5.224 -\newcommand{\isasymexists}{\isamath{\exists\,}}
5.225 -\newcommand{\isasymbox}{\isamath{\Box}} %requires amssymb
5.226 -\newcommand{\isasymdiamond}{\isamath{\Diamond}} %requires amssymb
5.227 -\newcommand{\isasymturnstile}{\isamath{\vdash}}
5.228 -\newcommand{\isasymTurnstile}{\isamath{\models}}
5.229 -\newcommand{\isasymtturnstile}{\isamath{\vdash\!\!\!\vdash}}
5.230 -\newcommand{\isasymTTurnstile}{\isamath{\mid\!\models}}
5.231 -\newcommand{\isasymstileturn}{\isamath{\dashv}}
5.232 -\newcommand{\isasymsurd}{\isamath{\surd}}
5.233 -\newcommand{\isasymle}{\isamath{\le}}
5.234 -\newcommand{\isasymge}{\isamath{\ge}}
5.235 -\newcommand{\isasymlless}{\isamath{\ll}}
5.236 -\newcommand{\isasymggreater}{\isamath{\gg}}
5.237 -\newcommand{\isasymlesssim}{\isamath{\lesssim}} %requires amssymb
5.238 -\newcommand{\isasymgreatersim}{\isamath{\gtrsim}} %requires amssymb
5.239 -\newcommand{\isasymlessapprox}{\isamath{\lessapprox}} %requires amssymb
5.240 -\newcommand{\isasymgreaterapprox}{\isamath{\gtrapprox}} %requires amssymb
5.241 -\newcommand{\isasymin}{\isamath{\in}}
5.242 -\newcommand{\isasymnotin}{\isamath{\notin}}
5.243 -\newcommand{\isasymsubset}{\isamath{\subset}}
5.244 -\newcommand{\isasymsupset}{\isamath{\supset}}
5.245 -\newcommand{\isasymsubseteq}{\isamath{\subseteq}}
5.246 -\newcommand{\isasymsupseteq}{\isamath{\supseteq}}
5.247 -\newcommand{\isasymsqsubset}{\isamath{\sqsubset}} %requires amssymb
5.248 -\newcommand{\isasymsqsupset}{\isamath{\sqsupset}} %requires amssymb
5.249 -\newcommand{\isasymsqsubseteq}{\isamath{\sqsubseteq}}
5.250 -\newcommand{\isasymsqsupseteq}{\isamath{\sqsupseteq}}
5.251 -\newcommand{\isasyminter}{\isamath{\cap}}
5.252 -\newcommand{\isasymInter}{\isamath{\bigcap\,}}
5.253 -\newcommand{\isasymunion}{\isamath{\cup}}
5.254 -\newcommand{\isasymUnion}{\isamath{\bigcup\,}}
5.255 -\newcommand{\isasymsqunion}{\isamath{\sqcup}}
5.256 -\newcommand{\isasymSqunion}{\isamath{\bigsqcup\,}}
5.257 -\newcommand{\isasymsqinter}{\isamath{\sqcap}}
5.258 -\newcommand{\isasymSqinter}{\isamath{\bigsqcap\,}} %requires amsmath
5.259 -\newcommand{\isasymuplus}{\isamath{\uplus}}
5.260 -\newcommand{\isasymUplus}{\isamath{\biguplus\,}}
5.261 -\newcommand{\isasymnoteq}{\isamath{\not=}}
5.262 -\newcommand{\isasymsim}{\isamath{\sim}}
5.263 -\newcommand{\isasymdoteq}{\isamath{\doteq}}
5.264 -\newcommand{\isasymsimeq}{\isamath{\simeq}}
5.265 -\newcommand{\isasymapprox}{\isamath{\approx}}
5.266 -\newcommand{\isasymasymp}{\isamath{\asymp}}
5.267 -\newcommand{\isasymcong}{\isamath{\cong}}
5.268 -\newcommand{\isasymsmile}{\isamath{\smile}}
5.269 -\newcommand{\isasymequiv}{\isamath{\equiv}}
5.270 -\newcommand{\isasymfrown}{\isamath{\frown}}
5.271 -\newcommand{\isasympropto}{\isamath{\propto}}
5.272 -\newcommand{\isasymsome}{\isamath{\epsilon\,}}
5.273 -\newcommand{\isasymJoin}{\isamath{\Join}} %requires amssymb
5.274 -\newcommand{\isasymbowtie}{\isamath{\bowtie}}
5.275 -\newcommand{\isasymprec}{\isamath{\prec}}
5.276 -\newcommand{\isasymsucc}{\isamath{\succ}}
5.277 -\newcommand{\isasympreceq}{\isamath{\preceq}}
5.278 -\newcommand{\isasymsucceq}{\isamath{\succeq}}
5.279 -\newcommand{\isasymparallel}{\isamath{\parallel}}
5.280 -\newcommand{\isasymbar}{\isamath{\mid}}
5.281 -\newcommand{\isasymplusminus}{\isamath{\pm}}
5.282 -\newcommand{\isasymminusplus}{\isamath{\mp}}
5.283 -\newcommand{\isasymtimes}{\isamath{\times}}
5.284 -\newcommand{\isasymdiv}{\isamath{\div}}
5.285 -\newcommand{\isasymcdot}{\isamath{\cdot}}
5.286 -\newcommand{\isasymstar}{\isamath{\star}}
5.287 -\newcommand{\isasymbullet}{\boldmath\isamath{\mathchoice{\displaystyle{\cdot}}{\textstyle{\cdot}}{\scriptstyle{\bullet}}{\scriptscriptstyle{\bullet}}}}
5.288 -\newcommand{\isasymcirc}{\isamath{\circ}}
5.289 -\newcommand{\isasymdagger}{\isamath{\dagger}}
5.290 -\newcommand{\isasymddagger}{\isamath{\ddagger}}
5.291 -\newcommand{\isasymlhd}{\isamath{\lhd}} %requires amssymb
5.292 -\newcommand{\isasymrhd}{\isamath{\rhd}} %requires amssymb
5.293 -\newcommand{\isasymunlhd}{\isamath{\unlhd}} %requires amssymb
5.294 -\newcommand{\isasymunrhd}{\isamath{\unrhd}} %requires amssymb
5.295 -\newcommand{\isasymtriangleleft}{\isamath{\triangleleft}}
5.296 -\newcommand{\isasymtriangleright}{\isamath{\triangleright}}
5.297 -\newcommand{\isasymtriangle}{\isamath{\triangle}}
5.298 -\newcommand{\isasymtriangleq}{\isamath{\triangleq}} %requires amssymb
5.299 -\newcommand{\isasymoplus}{\isamath{\oplus}}
5.300 -\newcommand{\isasymOplus}{\isamath{\bigoplus\,}}
5.301 -\newcommand{\isasymotimes}{\isamath{\otimes}}
5.302 -\newcommand{\isasymOtimes}{\isamath{\bigotimes\,}}
5.303 -\newcommand{\isasymodot}{\isamath{\odot}}
5.304 -\newcommand{\isasymOdot}{\isamath{\bigodot\,}}
5.305 -\newcommand{\isasymominus}{\isamath{\ominus}}
5.306 -\newcommand{\isasymoslash}{\isamath{\oslash}}
5.307 -\newcommand{\isasymdots}{\isamath{\dots}}
5.308 -\newcommand{\isasymcdots}{\isamath{\cdots}}
5.309 -\newcommand{\isasymSum}{\isamath{\sum\,}}
5.310 -\newcommand{\isasymProd}{\isamath{\prod\,}}
5.311 -\newcommand{\isasymCoprod}{\isamath{\coprod\,}}
5.312 -\newcommand{\isasyminfinity}{\isamath{\infty}}
5.313 -\newcommand{\isasymintegral}{\isamath{\int\,}}
5.314 -\newcommand{\isasymointegral}{\isamath{\oint\,}}
5.315 -\newcommand{\isasymclubsuit}{\isamath{\clubsuit}}
5.316 -\newcommand{\isasymdiamondsuit}{\isamath{\diamondsuit}}
5.317 -\newcommand{\isasymheartsuit}{\isamath{\heartsuit}}
5.318 -\newcommand{\isasymspadesuit}{\isamath{\spadesuit}}
5.319 -\newcommand{\isasymaleph}{\isamath{\aleph}}
5.320 -\newcommand{\isasymemptyset}{\isamath{\emptyset}}
5.321 -\newcommand{\isasymnabla}{\isamath{\nabla}}
5.322 -\newcommand{\isasympartial}{\isamath{\partial}}
5.323 -\newcommand{\isasymRe}{\isamath{\Re}}
5.324 -\newcommand{\isasymIm}{\isamath{\Im}}
5.325 -\newcommand{\isasymflat}{\isamath{\flat}}
5.326 -\newcommand{\isasymnatural}{\isamath{\natural}}
5.327 -\newcommand{\isasymsharp}{\isamath{\sharp}}
5.328 -\newcommand{\isasymangle}{\isamath{\angle}}
5.329 -\newcommand{\isasymcopyright}{\isatext{\rm\copyright}}
5.330 -\newcommand{\isasymregistered}{\isatext{\rm\textregistered}}
5.331 -\newcommand{\isasymhyphen}{\isatext{\rm-}}
5.332 -\newcommand{\isasyminverse}{\isamath{{}^{-1}}}
5.333 -\newcommand{\isasymonesuperior}{\isamath{\mathonesuperior}} %requires latin1
5.334 -\newcommand{\isasymonequarter}{\isatext{\rm\textonequarter}} %requires latin1
5.335 -\newcommand{\isasymtwosuperior}{\isamath{\mathtwosuperior}} %requires latin1
5.336 -\newcommand{\isasymonehalf}{\isatext{\rm\textonehalf}} %requires latin1
5.337 -\newcommand{\isasymthreesuperior}{\isamath{\maththreesuperior}} %requires latin1
5.338 -\newcommand{\isasymthreequarters}{\isatext{\rm\textthreequarters}} %requires latin1
5.339 -\newcommand{\isasymordfeminine}{\isatext{\rm\textordfeminine}}
5.340 -\newcommand{\isasymordmasculine}{\isatext{\rm\textordmasculine}}
5.341 -\newcommand{\isasymsection}{\isatext{\rm\S}}
5.342 -\newcommand{\isasymparagraph}{\isatext{\rm\P}}
5.343 -\newcommand{\isasymexclamdown}{\isatext{\rm\textexclamdown}}
5.344 -\newcommand{\isasymquestiondown}{\isatext{\rm\textquestiondown}}
5.345 -\newcommand{\isasymeuro}{\isatext{\textgreek{\euro}}} %requires greek babel
5.346 -\newcommand{\isasympounds}{\isamath{\pounds}}
5.347 -\newcommand{\isasymyen}{\isatext{\yen}} %requires amssymb
5.348 -\newcommand{\isasymcent}{\isatext{\textcent}} %requires textcomp
5.349 -\newcommand{\isasymcurrency}{\isatext{\textcurrency}} %requires textcomp
5.350 -\newcommand{\isasymdegree}{\isatext{\rm\textdegree}} %requires latin1
5.351 -\newcommand{\isasymamalg}{\isamath{\amalg}}
5.352 -\newcommand{\isasymmho}{\isamath{\mho}} %requires amssymb
5.353 -\newcommand{\isasymlozenge}{\isamath{\lozenge}} %requires amssymb
5.354 -\newcommand{\isasymwp}{\isamath{\wp}}
5.355 -\newcommand{\isasymwrong}{\isamath{\wr}}
5.356 -\newcommand{\isasymstruct}{\isamath{\diamond}}
5.357 -\newcommand{\isasymacute}{\isatext{\'\relax}}
5.358 -\newcommand{\isasymindex}{\isatext{\i}}
5.359 -\newcommand{\isasymdieresis}{\isatext{\"\relax}}
5.360 -\newcommand{\isasymcedilla}{\isatext{\c\relax}}
5.361 -\newcommand{\isasymhungarumlaut}{\isatext{\H\relax}}
5.362 -\newcommand{\isasymspacespace}{\isamath{~~}}
6.1 --- a/doc-src/LaTeXsugar/Sugar/generated/mathpartir.sty Sat Apr 30 02:43:45 2005 +0200
6.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
6.3 @@ -1,354 +0,0 @@
6.4 -%%
6.5 -%% This is the original source file mathpar.sty
6.6 -%%
6.7 -%% Package `mathpar' to use with LaTeX 2e
6.8 -%% Copyright Didier Remy, all rights reserved.
6.9 -\NeedsTeXFormat{LaTeX2e}
6.10 -\ProvidesPackage{mathpartir}
6.11 - [2001/23/02 v0.92 Math Paragraph for Type Inference Rules]
6.12 -
6.13 -%%
6.14 -
6.15 -%% Identification
6.16 -%% Preliminary declarations
6.17 -
6.18 -\RequirePackage {keyval}
6.19 -
6.20 -%% Options
6.21 -%% More declarations
6.22 -
6.23 -%% PART I: Typesetting maths in paragraphe mode
6.24 -
6.25 -\newdimen \mpr@tmpdim
6.26 -
6.27 -% To ensure hevea \hva compatibility, \hva should expands to nothing
6.28 -% in mathpar or in mathrule
6.29 -\let \mpr@hva \empty
6.30 -
6.31 -%% normal paragraph parametters, should rather be taken dynamically
6.32 -\def \mpr@savepar {%
6.33 - \edef \MathparNormalpar
6.34 - {\noexpand \lineskiplimit \the\lineskiplimit
6.35 - \noexpand \lineski \the\lineskip}%
6.36 - }
6.37 -
6.38 -\def \mpr@rulelineskip {\lineskiplimit=0.3em\lineskip=0.2em plus 0.1em}
6.39 -\def \mpr@lesslineskip {\lineskiplimit=0.6em\lineskip=0.5em plus 0.2em}
6.40 -\def \mpr@lineskip {\lineskiplimit=1.2em\lineskip=1.2em plus 0.2em}
6.41 -\let \MathparLineskip \mpr@lineskip
6.42 -\def \mpr@paroptions {\MathparLineskip}
6.43 -\let \mpr@prebindings \relax
6.44 -
6.45 -\newskip \mpr@andskip \mpr@andskip 2em plus 0.5fil minus 0.5em
6.46 -
6.47 -\def \mpr@goodbreakand
6.48 - {\hskip -\mpr@andskip \penalty -1000\hskip \mpr@andskip}
6.49 -\def \mpr@and {\hskip \mpr@andskip}
6.50 -\def \mpr@andcr {\penalty 50\mpr@and}
6.51 -\def \mpr@cr {\penalty -10000\mpr@and}
6.52 -\def \mpr@eqno #1{\mpr@andcr #1\hskip 0em plus -1fil \penalty 10}
6.53 -
6.54 -\def \mpr@bindings {%
6.55 - \let \and \mpr@andcr
6.56 - \let \par \mpr@andcr
6.57 - \let \\\mpr@cr
6.58 - \let \eqno \mpr@eqno
6.59 - \let \hva \mpr@hva
6.60 - }
6.61 -\let \MathparBindings \mpr@bindings
6.62 -
6.63 -\newenvironment{mathpar}[1][]
6.64 - {$$\mpr@savepar \parskip 0em \hsize \linewidth \centering
6.65 - \vbox \bgroup \mpr@prebindings \mpr@paroptions #1\ifmmode $\else
6.66 - \noindent $\displaystyle\fi
6.67 - \MathparBindings}
6.68 - {\unskip \ifmmode $\fi\egroup $$\ignorespacesafterend}
6.69 -
6.70 -% \def \math@mathpar #1{\setbox0 \hbox {$\displaystyle #1$}\ifnum
6.71 -% \wd0 < \hsize $$\box0$$\else \bmathpar #1\emathpar \fi}
6.72 -
6.73 -%%% HOV BOXES
6.74 -
6.75 -\def \mathvbox@ #1{\hbox \bgroup \mpr@normallineskip
6.76 - \vbox \bgroup \tabskip 0em \let \\ \cr
6.77 - \halign \bgroup \hfil $##$\hfil\cr #1\crcr \egroup \egroup
6.78 - \egroup}
6.79 -
6.80 -\def \mathhvbox@ #1{\setbox0 \hbox {\let \\\qquad $#1$}\ifnum \wd0 < \hsize
6.81 - \box0\else \mathvbox {#1}\fi}
6.82 -
6.83 -
6.84 -%% Part II -- operations on lists
6.85 -
6.86 -\newtoks \mpr@lista
6.87 -\newtoks \mpr@listb
6.88 -
6.89 -\long \def\mpr@cons #1\to#2{\mpr@lista {\\{#1}}\mpr@listb \expandafter
6.90 -{#2}\edef #2{\the \mpr@lista \the \mpr@listb}}
6.91 -
6.92 -\long \def\mpr@snoc #1\to#2{\mpr@lista {\\{#1}}\mpr@listb \expandafter
6.93 -{#2}\edef #2{\the \mpr@listb\the\mpr@lista}}
6.94 -
6.95 -\long \def \mpr@concat#1=#2\to#3{\mpr@lista \expandafter {#2}\mpr@listb
6.96 -\expandafter {#3}\edef #1{\the \mpr@listb\the\mpr@lista}}
6.97 -
6.98 -\def \mpr@head #1\to #2{\expandafter \mpr@head@ #1\mpr@head@ #1#2}
6.99 -\long \def \mpr@head@ #1#2\mpr@head@ #3#4{\def #4{#1}\def#3{#2}}
6.100 -
6.101 -\def \mpr@flatten #1\to #2{\expandafter \mpr@flatten@ #1\mpr@flatten@ #1#2}
6.102 -\long \def \mpr@flatten@ \\#1\\#2\mpr@flatten@ #3#4{\def #4{#1}\def #3{\\#2}}
6.103 -
6.104 -\def \mpr@makelist #1\to #2{\def \mpr@all {#1}%
6.105 - \mpr@lista {\\}\mpr@listb \expandafter {\mpr@all}\edef \mpr@all {\the
6.106 - \mpr@lista \the \mpr@listb \the \mpr@lista}\let #2\empty
6.107 - \def \mpr@stripof ##1##2\mpr@stripend{\def \mpr@stripped{##2}}\loop
6.108 - \mpr@flatten \mpr@all \to \mpr@one
6.109 - \expandafter \mpr@snoc \mpr@one \to #2\expandafter \mpr@stripof
6.110 - \mpr@all \mpr@stripend
6.111 - \ifx \mpr@stripped \empty \let \mpr@isempty 0\else \let \mpr@isempty 1\fi
6.112 - \ifx 1\mpr@isempty
6.113 - \repeat
6.114 -}
6.115 -
6.116 -%% Part III -- Type inference rules
6.117 -
6.118 -\def \mpr@rev #1\to #2{\let \mpr@tmp \empty
6.119 - \def \\##1{\mpr@cons ##1\to \mpr@tmp}#1\let #2\mpr@tmp}
6.120 -
6.121 -\newif \if@premisse
6.122 -\newbox \mpr@hlist
6.123 -\newbox \mpr@vlist
6.124 -\newif \ifmpr@center \mpr@centertrue
6.125 -\def \mpr@htovlist {%
6.126 - \setbox \mpr@hlist
6.127 - \hbox {\strut
6.128 - \ifmpr@center \hskip -0.5\wd\mpr@hlist\fi
6.129 - \unhbox \mpr@hlist}%
6.130 - \setbox \mpr@vlist
6.131 - \vbox {\if@premisse \box \mpr@hlist \unvbox \mpr@vlist
6.132 - \else \unvbox \mpr@vlist \box \mpr@hlist
6.133 - \fi}%
6.134 -}
6.135 -% OLD version
6.136 -% \def \mpr@htovlist {%
6.137 -% \setbox \mpr@hlist
6.138 -% \hbox {\strut \hskip -0.5\wd\mpr@hlist \unhbox \mpr@hlist}%
6.139 -% \setbox \mpr@vlist
6.140 -% \vbox {\if@premisse \box \mpr@hlist \unvbox \mpr@vlist
6.141 -% \else \unvbox \mpr@vlist \box \mpr@hlist
6.142 -% \fi}%
6.143 -% }
6.144 -
6.145 -
6.146 -
6.147 -
6.148 -\def \mpr@blank { }
6.149 -\def \mpr@hovbox #1#2{\hbox
6.150 - \bgroup
6.151 - \ifx #1T\@premissetrue
6.152 - \else \ifx #1B\@premissefalse
6.153 - \else
6.154 - \PackageError{mathpartir}
6.155 - {Premisse orientation should either be P or B}
6.156 - {Fatal error in Package}%
6.157 - \fi \fi
6.158 - \def \@test {#2}\ifx \@test \mpr@blank\else
6.159 - \setbox \mpr@hlist \hbox {}%
6.160 - \setbox \mpr@vlist \vbox {}%
6.161 - \if@premisse \let \snoc \mpr@cons \else \let \snoc \mpr@snoc \fi
6.162 - \let \@hvlist \empty \let \@rev \empty
6.163 - \mpr@tmpdim 0em
6.164 - \expandafter \mpr@makelist #2\to \mpr@flat
6.165 - \if@premisse \mpr@rev \mpr@flat \to \@rev \else \let \@rev \mpr@flat \fi
6.166 - \def \\##1{%
6.167 - \def \@test {##1}\ifx \@test \empty
6.168 - \mpr@htovlist
6.169 - \mpr@tmpdim 0em %%% last bug fix not extensively checked
6.170 - \else
6.171 - \setbox0 \hbox{$\displaystyle {##1}$}\relax
6.172 - \advance \mpr@tmpdim by \wd0
6.173 - %\mpr@tmpdim 1.02\mpr@tmpdim
6.174 - \ifnum \mpr@tmpdim < \hsize
6.175 - \ifnum \wd\mpr@hlist > 0
6.176 - \if@premisse
6.177 - \setbox \mpr@hlist \hbox {\unhbox0 \qquad \unhbox \mpr@hlist}%
6.178 - \else
6.179 - \setbox \mpr@hlist \hbox {\unhbox \mpr@hlist \qquad \unhbox0}%
6.180 - \fi
6.181 - \else
6.182 - \setbox \mpr@hlist \hbox {\unhbox0}%
6.183 - \fi
6.184 - \else
6.185 - \ifnum \wd \mpr@hlist > 0
6.186 - \mpr@htovlist
6.187 - \mpr@tmpdim \wd0
6.188 - \fi
6.189 - \setbox \mpr@hlist \hbox {\unhbox0}%
6.190 - \fi
6.191 - \advance \mpr@tmpdim by 2em
6.192 - \fi
6.193 - }%
6.194 - \@rev
6.195 - \mpr@htovlist
6.196 - \ifmpr@center \hskip \wd\mpr@vlist\fi \box \mpr@vlist
6.197 - \fi
6.198 - \egroup
6.199 -}
6.200 -
6.201 -%%% INFERENCE RULES
6.202 -
6.203 -\@ifundefined{@@over}{%
6.204 - \let\@@over\over % fallback if amsmath is not loaded
6.205 - \let\@@overwithdelims\overwithdelims
6.206 - \let\@@atop\atop \let\@@atopwithdelims\atopwithdelims
6.207 - \let\@@above\above \let\@@abovewithdelims\abovewithdelims
6.208 - }{}
6.209 -
6.210 -
6.211 -\def \mpr@@fraction #1#2{\hbox {\advance \hsize by -0.5em
6.212 - $\displaystyle {#1\@@over #2}$}}
6.213 -\let \mpr@fraction \mpr@@fraction
6.214 -\def \mpr@@reduce #1#2{\hbox
6.215 - {$\lower 0.01pt \mpr@@fraction {#1}{#2}\mkern -15mu\rightarrow$}}
6.216 -\def \mpr@infercenter #1{\vcenter {\mpr@hovbox{T}{#1}}}
6.217 -
6.218 -\def \mpr@empty {}
6.219 -\def \mpr@inferrule
6.220 - {\bgroup
6.221 - \mpr@rulelineskip
6.222 - \let \and \qquad
6.223 - \let \hva \mpr@hva
6.224 - \let \@rulename \mpr@empty
6.225 - \let \@rule@options \mpr@empty
6.226 - \mpr@inferrule@}
6.227 -\newcommand {\mpr@inferrule@}[3][]
6.228 - {\everymath={\displaystyle}%
6.229 - \def \@test {#2}\ifx \empty \@test
6.230 - \setbox0 \hbox {$\vcenter {\mpr@hovbox{B}{#3}}$}%
6.231 - \else
6.232 - \def \@test {#3}\ifx \empty \@test
6.233 - \setbox0 \hbox {$\vcenter {\mpr@hovbox{T}{#2}}$}%
6.234 - \else
6.235 - \setbox0 \mpr@fraction {\mpr@hovbox{T}{#2}}{\mpr@hovbox{B}{#3}}%
6.236 - \fi \fi
6.237 - \def \@test {#1}\ifx \@test\empty \box0
6.238 - \else \vbox
6.239 -%%% Suggestion de Francois pour les etiquettes longues
6.240 -%%% {\hbox to \wd0 {\TirName {#1}\hfil}\box0}\fi
6.241 - {\hbox {\TirName {#1}}\box0}\fi
6.242 - \egroup}
6.243 -
6.244 -\def \mpr@vdotfil #1{\vbox to #1{\leaders \hbox{$\cdot$} \vfil}}
6.245 -
6.246 -% They are two forms
6.247 -% \mathrule [label]{[premisses}{conclusions}
6.248 -% or
6.249 -% \mathrule* [options]{[premisses}{conclusions}
6.250 -%
6.251 -% Premisses and conclusions are lists of elements separated by \\
6.252 -% Each \\ produces a break, attempting horizontal breaks if possible,
6.253 -% and vertical breaks if needed.
6.254 -%
6.255 -% An empty element obtained by \\\\ produces a vertical break in all cases.
6.256 -%
6.257 -% The former rule is aligned on the fraction bar.
6.258 -% The optional label appears on top of the rule
6.259 -% The second form to be used in a derivation tree is aligned on the last
6.260 -% line of its conclusion
6.261 -%
6.262 -% The second form can be parameterized, using the key=val interface. The
6.263 -% folloiwng keys are recognized:
6.264 -%
6.265 -% width set the width of the rule to val
6.266 -% narrower set the width of the rule to val\hsize
6.267 -% before execute val at the beginning/left
6.268 -% lab put a label [Val] on top of the rule
6.269 -% lskip add negative skip on the right
6.270 -% llab put a left label [Val], ignoring its width
6.271 -% left put a left label [Val]
6.272 -% right put a right label [Val]
6.273 -% rlab put a right label [Val], ignoring its width
6.274 -% rskip add negative skip on the left
6.275 -% vdots lift the rule by val and fill vertical space with dots
6.276 -% after execute val at the end/right
6.277 -%
6.278 -% Note that most options must come in this order to avoid strange
6.279 -% typesetting (in particular lskip must preceed left and llab and
6.280 -% rskip must follow rlab or right; vdots must come last or be followed by
6.281 -% rskip.
6.282 -%
6.283 -
6.284 -\define@key {mprset}{flushleft}[]{\mpr@centerfalse}
6.285 -\define@key {mprset}{center}[]{\mpr@centertrue}
6.286 -\def \mprset #1{\setkeys{mprset}{#1}}
6.287 -
6.288 -\newbox \mpr@right
6.289 -\define@key {mpr}{flushleft}[]{\mpr@centerfalse}
6.290 -\define@key {mpr}{center}[]{\mpr@centertrue}
6.291 -\define@key {mpr}{left}{\setbox0 \hbox {$\TirName {#1}\;$}\relax
6.292 - \advance \hsize by -\wd0\box0}
6.293 -\define@key {mpr}{width}{\hsize #1}
6.294 -\define@key {mpr}{before}{#1}
6.295 -\define@key {mpr}{lab}{\def \mpr@rulename {[#1]}}
6.296 -\define@key {mpr}{Lab}{\def \mpr@rulename {#1}}
6.297 -\define@key {mpr}{narrower}{\hsize #1\hsize}
6.298 -\define@key {mpr}{leftskip}{\hskip -#1}
6.299 -\define@key {mpr}{reduce}[]{\let \mpr@fraction \mpr@@reduce}
6.300 -\define@key {mpr}{rightskip}
6.301 - {\setbox \mpr@right \hbox {\unhbox \mpr@right \hskip -#1}}
6.302 -\define@key {mpr}{left}{\setbox0 \hbox {$\TirName {#1}\;$}\relax
6.303 - \advance \hsize by -\wd0\box0}
6.304 -\define@key {mpr}{Left}{\llap{$\TirName {#1}\;$}}
6.305 -\define@key {mpr}{right}
6.306 - {\setbox0 \hbox {$\;\TirName {#1}$}\relax \advance \hsize by -\wd0
6.307 - \setbox \mpr@right \hbox {\unhbox \mpr@right \unhbox0}}
6.308 -\define@key {mpr}{Right}
6.309 - {\setbox \mpr@right \hbox {\unhbox \mpr@right \rlap {$\;\TirName {#1}$}}}
6.310 -\define@key {mpr}{vdots}{\def \mpr@vdots {\@@atop \mpr@vdotfil{#1}}}
6.311 -\define@key {mpr}{after}{\edef \mpr@after {\mpr@after #1}}
6.312 -
6.313 -\newdimen \rule@dimen
6.314 -\newcommand \mpr@inferstar@ [3][]{\setbox0
6.315 - \hbox {\let \mpr@rulename \mpr@empty \let \mpr@vdots \relax
6.316 - \setbox \mpr@right \hbox{}%
6.317 - $\setkeys{mpr}{#1}%
6.318 - \ifx \mpr@rulename \mpr@empty \mpr@inferrule {#2}{#3}\else
6.319 - \mpr@inferrule [{\mpr@rulename}]{#2}{#3}\fi
6.320 - \box \mpr@right \mpr@vdots$}
6.321 - \setbox1 \hbox {\strut}
6.322 - \rule@dimen \dp0 \advance \rule@dimen by -\dp1
6.323 - \raise \rule@dimen \box0}
6.324 -
6.325 -\def \mpr@infer {\@ifnextchar *{\mpr@inferstar}{\mpr@inferrule}}
6.326 -\newcommand \mpr@err@skipargs[3][]{}
6.327 -\def \mpr@inferstar*{\ifmmode
6.328 - \let \@do \mpr@inferstar@
6.329 - \else
6.330 - \let \@do \mpr@err@skipargs
6.331 - \PackageError {mathpartir}
6.332 - {\string\inferrule* can only be used in math mode}{}%
6.333 - \fi \@do}
6.334 -
6.335 -
6.336 -%%% Exports
6.337 -
6.338 -% Envirnonment mathpar
6.339 -
6.340 -\let \inferrule \mpr@infer
6.341 -
6.342 -% make a short name \infer is not already defined
6.343 -\@ifundefined {infer}{\let \infer \mpr@infer}{}
6.344 -
6.345 -\def \tir@name #1{\hbox {\small \sc #1}}
6.346 -\let \TirName \tir@name
6.347 -
6.348 -%%% Other Exports
6.349 -
6.350 -% \let \listcons \mpr@cons
6.351 -% \let \listsnoc \mpr@snoc
6.352 -% \let \listhead \mpr@head
6.353 -% \let \listmake \mpr@makelist
6.354 -
6.355 -
6.356 -\endinput
6.357 -
7.1 --- a/doc-src/LaTeXsugar/Sugar/generated/pdfsetup.sty Sat Apr 30 02:43:45 2005 +0200
7.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
7.3 @@ -1,11 +0,0 @@
7.4 -%%
7.5 -%% Author: Markus Wenzel, TU Muenchen
7.6 -%%
7.7 -%% smart url or hyperref setup
7.8 -%%
7.9 -
7.10 -\@ifundefined{pdfoutput}
7.11 -{\usepackage{url}}
7.12 -{\usepackage{color}\definecolor{darkblue}{rgb}{0,0,0.5}
7.13 - \usepackage[pdftex,a4paper,colorlinks=true,linkcolor=darkblue,citecolor=darkblue,filecolor=darkblue,pagecolor=darkblue,urlcolor=darkblue]{hyperref}
7.14 - \IfFileExists{thumbpdf.sty}{\usepackage{thumbpdf}}{}}
8.1 --- a/doc-src/LaTeXsugar/Sugar/generated/root.bib Sat Apr 30 02:43:45 2005 +0200
8.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
8.3 @@ -1,12 +0,0 @@
8.4 -@book{LNCS2283,author={Tobias Nipkow and Lawrence Paulson and Markus Wenzel},
8.5 -title="Isabelle/HOL --- A Proof Assistant for Higher-Order Logic",
8.6 -publisher=Springer,series=LNCS,volume=2283,year=2002,
8.7 -note={\url{http://www.in.tum.de/~nipkow/LNCS2283/}}}
8.8 -
8.9 -@misc{mathpartir,author={Didier R\'emy},title={mathpartir},
8.10 -note={\url{http://cristal.inria.fr/~remy/latex/}}}
8.11 -
8.12 -@misc{tar,author={Gerwin Klein and Norber Schirmer and Tobias Nipkow},
8.13 -title={{LaTeX} sugar theories and support files},
8.14 -note={\url{http://isabelle.in.tum.de/sugar.tar.gz}}}
8.15 -
9.1 --- a/doc-src/LaTeXsugar/Sugar/generated/root.tex Sat Apr 30 02:43:45 2005 +0200
9.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
9.3 @@ -1,59 +0,0 @@
9.4 -\documentclass[11pt,a4paper]{article}
9.5 -\usepackage{isabelle,isabellesym}
9.6 -
9.7 -% further packages required for unusual symbols (see also isabellesym.sty)
9.8 -% use only when needed
9.9 -%\usepackage{amssymb} % for \<leadsto>, \<box>, \<diamond>,
9.10 - % \<sqsupset>, \<mho>, \<Join>,
9.11 - % \<lhd>, \<lesssim>, \<greatersim>,
9.12 - % \<lessapprox>, \<greaterapprox>,
9.13 - % \<triangleq>, \<yen>, \<lozenge>
9.14 -%\usepackage[greek,english]{babel} % greek for \<euro>,
9.15 - % english for \<guillemotleft>,
9.16 - % \<guillemotright>
9.17 - % default language = last
9.18 -%\usepackage[latin1]{inputenc} % for \<onesuperior>, \<onequarter>,
9.19 - % \<twosuperior>, \<onehalf>,
9.20 - % \<threesuperior>, \<threequarters>,
9.21 - % \<degree>
9.22 -%\usepackage[only,bigsqcap]{stmaryrd} % for \<Sqinter>
9.23 -%\usepackage{eufrak} % for \<AA> ... \<ZZ>, \<aa> ... \<zz>
9.24 - % (only needed if amssymb not used)
9.25 -%\usepackage{textcomp} % for \<cent>, \<currency>
9.26 -
9.27 -\usepackage{mathpartir}
9.28 -
9.29 -% this should be the last package used
9.30 -\usepackage{pdfsetup}
9.31 -
9.32 -% urls in roman style, theory text in math-similar italics
9.33 -\urlstyle{rm}
9.34 -\isabellestyle{it}
9.35 -
9.36 -\hyphenation{Isa-belle}
9.37 -\begin{document}
9.38 -
9.39 -\title{\LaTeX\ Sugar for Isabelle documents}
9.40 -\author{Gerwin Klein, Tobias Nipkow, Norbert Schirmer}
9.41 -\maketitle
9.42 -
9.43 -\begin{abstract}
9.44 -This document shows how to typset mathematics in Isabelle-based
9.45 -documents in a style close to that in ordinary computer science papers.
9.46 -\end{abstract}
9.47 -
9.48 -\tableofcontents
9.49 -
9.50 -% generated text of all theories
9.51 -\input{Sugar.tex}
9.52 -
9.53 -% optional bibliography
9.54 -\bibliographystyle{abbrv}
9.55 -\bibliography{root}
9.56 -
9.57 -\end{document}
9.58 -
9.59 -%%% Local Variables:
9.60 -%%% mode: latex
9.61 -%%% TeX-master: t
9.62 -%%% End:
10.1 --- a/doc-src/LaTeXsugar/Sugar/generated/session.tex Sat Apr 30 02:43:45 2005 +0200
10.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
10.3 @@ -1,10 +0,0 @@
10.4 -\input{LaTeXsugar.tex}
10.5 -
10.6 -\input{OptionalSugar.tex}
10.7 -
10.8 -\input{Sugar.tex}
10.9 -
10.10 -%%% Local Variables:
10.11 -%%% mode: latex
10.12 -%%% TeX-master: "root"
10.13 -%%% End: