1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/doc-src/LaTeXsugar/IsaMakefile Mon Nov 29 11:12:19 2004 +0100
1.3 @@ -0,0 +1,31 @@
1.4 +
1.5 +## targets
1.6 +
1.7 +default: Sugar
1.8 +images:
1.9 +test: Sugar
1.10 +
1.11 +all: images test
1.12 +
1.13 +
1.14 +## global settings
1.15 +
1.16 +SRC = $(ISABELLE_HOME)/src
1.17 +OUT = $(ISABELLE_OUTPUT)
1.18 +LOG = $(OUT)/log
1.19 +
1.20 +USEDIR = $(ISATOOL) usedir -v true -i true -d pdf -D generated
1.21 +
1.22 +
1.23 +## Sugar
1.24 +
1.25 +Sugar: $(LOG)/HOL-Sugar.gz
1.26 +
1.27 +$(LOG)/HOL-Sugar.gz: Sugar/ROOT.ML Sugar/document/root.tex Sugar/*.thy
1.28 + @$(USEDIR) HOL Sugar
1.29 +
1.30 +
1.31 +## clean
1.32 +
1.33 +clean:
1.34 + @rm -f $(LOG)/HOL-Sugar.gz
2.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
2.2 +++ b/doc-src/LaTeXsugar/Sugar/ROOT.ML Mon Nov 29 11:12:19 2004 +0100
2.3 @@ -0,0 +1,2 @@
2.4 +use_thy "Sugar";
2.5 +
3.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
3.2 +++ b/doc-src/LaTeXsugar/Sugar/Sugar.thy Mon Nov 29 11:12:19 2004 +0100
3.3 @@ -0,0 +1,102 @@
3.4 +(*<*)
3.5 +theory Sugar
3.6 +imports Main
3.7 +begin
3.8 +(*>*)
3.9 +
3.10 +section "Introduction"
3.11 +
3.12 +text{* This document is for those Isabelle users that have mastered
3.13 +the art of mixing \LaTeX\ text and Isabelle theories and never want to
3.14 +typeset a theorem by hand anymore because they have experienced the
3.15 +bliss of writing \verb!@!\verb!{thm[display]setsum_cartesian_product[no_vars]}!
3.16 +and seeing Isabelle typeset it for them:
3.17 +@{thm[display,eta_contract=false] setsum_cartesian_product[no_vars]}
3.18 +No typos, no omissions, no sweat!
3.19 +If you have not experienced that joy, read chapter 4, \emph{Presenting
3.20 +Theories}, of \cite{LNCS2283} first.
3.21 +
3.22 +If you have mastered the art of Isabelle's \emph{antiquotations},
3.23 +i.e.\ things like the above \verb!@!\verb!{thm...}!, beware: in your vanity
3.24 +you may be tempted to think that all readers of the stunning ps or pdf
3.25 +documents you can now produce at the drop of a hat will be struck with
3.26 +awe at the beauty unfolding in front of their eyes. Until one day you
3.27 +come across that very critical of readers known as the ``common referee''.
3.28 +He has the nasty habit of refusing to understand unfamiliar notation
3.29 +like Isabelle's infamous @{text"\<lbrakk> \<rbrakk> \<Longrightarrow>"} no matter how many times you
3.30 +explain it in your paper. Even worse, he thinks that using @{text"\<lbrakk>
3.31 +\<rbrakk>"} for anything other than denotational semantics is a cardinal sin
3.32 +that must be punished by immediate rejection.
3.33 +
3.34 +
3.35 +This document shows you how to make Isabelle and \LaTeX\ cooperate to
3.36 +produce ordinary looking mathematics that hides the fact that it was
3.37 +typeset by a machine. This involves additional syntax-related
3.38 +declarations for your theory file and corresponding \LaTeX\ macros. We
3.39 +explain how to use them but show neither. They can be downloaded from
3.40 +the web.
3.41 +
3.42 +*}
3.43 +
3.44 +section "Printing theorems"
3.45 +
3.46 +subsection "Inference rules"
3.47 +
3.48 +(*<*)
3.49 +syntax (Rule output)
3.50 + "==>" :: "prop \<Rightarrow> prop \<Rightarrow> prop"
3.51 + ("\<^raw:\mbox{}\inferrule{>_\<^raw:}>\<^raw:{>_\<^raw:}>")
3.52 +
3.53 + "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
3.54 + ("\<^raw:\mbox{}\inferrule{>_\<^raw:}>\<^raw:{>_\<^raw:}>")
3.55 +
3.56 + "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms"
3.57 + ("_\<^raw:\\>/ _")
3.58 +
3.59 + "_asm" :: "prop \<Rightarrow> asms" ("_")
3.60 +(*>*)
3.61 +
3.62 +text{* To print theorems as inference rules you need to include the
3.63 +\texttt{Rule} output syntax declarations in your theory and Didier
3.64 +Remy's \texttt{mathpartir} package for typesetting inference rules in
3.65 +your \LaTeX\ file.
3.66 +
3.67 +Writing \verb!@!\verb!{thm[mode=Rule] conjI[no_vars]}! produces
3.68 +@{thm[mode=Rule] conjI[no_vars]}, even in the middle of a sentence.
3.69 +The standard \texttt{display} attribute, i.e.\ writing
3.70 +\verb![mode=Rule,display]! instead of \verb![mode=Rule]!,
3.71 +displays the rule on a separate line using a smaller font:
3.72 +@{thm[mode=Rule,display] conjI[no_vars]}
3.73 +Centering a display does not work directly. Instead you can enclose the
3.74 +non-displayed variant in a \texttt{center} environment:
3.75 +
3.76 +\begin{quote}
3.77 +\verb!\begin{center}!\\
3.78 +\verb!@!\verb!{thm[mode=Rule] conjI[no_vars]} {\sc conjI}!\\
3.79 +\verb!\end{center}!
3.80 +\end{quote}
3.81 +also adds a label to the rule and yields
3.82 +\begin{center}
3.83 +@{thm[mode=Rule] conjI[no_vars]} {\sc conjI}
3.84 +\end{center}
3.85 +Of course you can display multiple rules in this fashion:
3.86 +\begin{quote}
3.87 +\verb!\begin{center}\isastyle!\\
3.88 +\verb!@!\verb!{thm[mode=Rule] conjI[no_vars]} {\sc conjI} \\[1ex]!\\
3.89 +\verb!@!\verb!{thm[mode=Rule] conjE[no_vars]} {\sc disjI$_1$} \qquad!\\
3.90 +\verb!@!\verb!{thm[mode=Rule] disjE[no_vars]} {\sc disjI$_2$}!\\
3.91 +\verb!\end{center}!
3.92 +\end{quote}
3.93 +yields
3.94 +\begin{center}\isastyle
3.95 +@{thm[mode=Rule] conjI[no_vars]} {\sc conjI} \\[1ex]
3.96 +@{thm[mode=Rule] disjI1[no_vars]} {\sc disjI$_1$} \qquad
3.97 +@{thm[mode=Rule] disjI2[no_vars]} {\sc disjI$_2$}
3.98 +\end{center}
3.99 +Note that we included \verb!\isastyle! to obtain
3.100 +the smaller font that otherwise comes only with \texttt{display}.
3.101 +
3.102 +*}
3.103 +(*<*)
3.104 +end
3.105 +(*>*)
3.106 \ No newline at end of file
4.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
4.2 +++ b/doc-src/LaTeXsugar/Sugar/document/mathpartir.sty Mon Nov 29 11:12:19 2004 +0100
4.3 @@ -0,0 +1,354 @@
4.4 +%%
4.5 +%% This is the original source file mathpar.sty
4.6 +%%
4.7 +%% Package `mathpar' to use with LaTeX 2e
4.8 +%% Copyright Didier Remy, all rights reserved.
4.9 +\NeedsTeXFormat{LaTeX2e}
4.10 +\ProvidesPackage{mathpartir}
4.11 + [2001/23/02 v0.92 Math Paragraph for Type Inference Rules]
4.12 +
4.13 +%%
4.14 +
4.15 +%% Identification
4.16 +%% Preliminary declarations
4.17 +
4.18 +\RequirePackage {keyval}
4.19 +
4.20 +%% Options
4.21 +%% More declarations
4.22 +
4.23 +%% PART I: Typesetting maths in paragraphe mode
4.24 +
4.25 +\newdimen \mpr@tmpdim
4.26 +
4.27 +% To ensure hevea \hva compatibility, \hva should expands to nothing
4.28 +% in mathpar or in mathrule
4.29 +\let \mpr@hva \empty
4.30 +
4.31 +%% normal paragraph parametters, should rather be taken dynamically
4.32 +\def \mpr@savepar {%
4.33 + \edef \MathparNormalpar
4.34 + {\noexpand \lineskiplimit \the\lineskiplimit
4.35 + \noexpand \lineski \the\lineskip}%
4.36 + }
4.37 +
4.38 +\def \mpr@rulelineskip {\lineskiplimit=0.3em\lineskip=0.2em plus 0.1em}
4.39 +\def \mpr@lesslineskip {\lineskiplimit=0.6em\lineskip=0.5em plus 0.2em}
4.40 +\def \mpr@lineskip {\lineskiplimit=1.2em\lineskip=1.2em plus 0.2em}
4.41 +\let \MathparLineskip \mpr@lineskip
4.42 +\def \mpr@paroptions {\MathparLineskip}
4.43 +\let \mpr@prebindings \relax
4.44 +
4.45 +\newskip \mpr@andskip \mpr@andskip 2em plus 0.5fil minus 0.5em
4.46 +
4.47 +\def \mpr@goodbreakand
4.48 + {\hskip -\mpr@andskip \penalty -1000\hskip \mpr@andskip}
4.49 +\def \mpr@and {\hskip \mpr@andskip}
4.50 +\def \mpr@andcr {\penalty 50\mpr@and}
4.51 +\def \mpr@cr {\penalty -10000\mpr@and}
4.52 +\def \mpr@eqno #1{\mpr@andcr #1\hskip 0em plus -1fil \penalty 10}
4.53 +
4.54 +\def \mpr@bindings {%
4.55 + \let \and \mpr@andcr
4.56 + \let \par \mpr@andcr
4.57 + \let \\\mpr@cr
4.58 + \let \eqno \mpr@eqno
4.59 + \let \hva \mpr@hva
4.60 + }
4.61 +\let \MathparBindings \mpr@bindings
4.62 +
4.63 +\newenvironment{mathpar}[1][]
4.64 + {$$\mpr@savepar \parskip 0em \hsize \linewidth \centering
4.65 + \vbox \bgroup \mpr@prebindings \mpr@paroptions #1\ifmmode $\else
4.66 + \noindent $\displaystyle\fi
4.67 + \MathparBindings}
4.68 + {\unskip \ifmmode $\fi\egroup $$\ignorespacesafterend}
4.69 +
4.70 +% \def \math@mathpar #1{\setbox0 \hbox {$\displaystyle #1$}\ifnum
4.71 +% \wd0 < \hsize $$\box0$$\else \bmathpar #1\emathpar \fi}
4.72 +
4.73 +%%% HOV BOXES
4.74 +
4.75 +\def \mathvbox@ #1{\hbox \bgroup \mpr@normallineskip
4.76 + \vbox \bgroup \tabskip 0em \let \\ \cr
4.77 + \halign \bgroup \hfil $##$\hfil\cr #1\crcr \egroup \egroup
4.78 + \egroup}
4.79 +
4.80 +\def \mathhvbox@ #1{\setbox0 \hbox {\let \\\qquad $#1$}\ifnum \wd0 < \hsize
4.81 + \box0\else \mathvbox {#1}\fi}
4.82 +
4.83 +
4.84 +%% Part II -- operations on lists
4.85 +
4.86 +\newtoks \mpr@lista
4.87 +\newtoks \mpr@listb
4.88 +
4.89 +\long \def\mpr@cons #1\to#2{\mpr@lista {\\{#1}}\mpr@listb \expandafter
4.90 +{#2}\edef #2{\the \mpr@lista \the \mpr@listb}}
4.91 +
4.92 +\long \def\mpr@snoc #1\to#2{\mpr@lista {\\{#1}}\mpr@listb \expandafter
4.93 +{#2}\edef #2{\the \mpr@listb\the\mpr@lista}}
4.94 +
4.95 +\long \def \mpr@concat#1=#2\to#3{\mpr@lista \expandafter {#2}\mpr@listb
4.96 +\expandafter {#3}\edef #1{\the \mpr@listb\the\mpr@lista}}
4.97 +
4.98 +\def \mpr@head #1\to #2{\expandafter \mpr@head@ #1\mpr@head@ #1#2}
4.99 +\long \def \mpr@head@ #1#2\mpr@head@ #3#4{\def #4{#1}\def#3{#2}}
4.100 +
4.101 +\def \mpr@flatten #1\to #2{\expandafter \mpr@flatten@ #1\mpr@flatten@ #1#2}
4.102 +\long \def \mpr@flatten@ \\#1\\#2\mpr@flatten@ #3#4{\def #4{#1}\def #3{\\#2}}
4.103 +
4.104 +\def \mpr@makelist #1\to #2{\def \mpr@all {#1}%
4.105 + \mpr@lista {\\}\mpr@listb \expandafter {\mpr@all}\edef \mpr@all {\the
4.106 + \mpr@lista \the \mpr@listb \the \mpr@lista}\let #2\empty
4.107 + \def \mpr@stripof ##1##2\mpr@stripend{\def \mpr@stripped{##2}}\loop
4.108 + \mpr@flatten \mpr@all \to \mpr@one
4.109 + \expandafter \mpr@snoc \mpr@one \to #2\expandafter \mpr@stripof
4.110 + \mpr@all \mpr@stripend
4.111 + \ifx \mpr@stripped \empty \let \mpr@isempty 0\else \let \mpr@isempty 1\fi
4.112 + \ifx 1\mpr@isempty
4.113 + \repeat
4.114 +}
4.115 +
4.116 +%% Part III -- Type inference rules
4.117 +
4.118 +\def \mpr@rev #1\to #2{\let \mpr@tmp \empty
4.119 + \def \\##1{\mpr@cons ##1\to \mpr@tmp}#1\let #2\mpr@tmp}
4.120 +
4.121 +\newif \if@premisse
4.122 +\newbox \mpr@hlist
4.123 +\newbox \mpr@vlist
4.124 +\newif \ifmpr@center \mpr@centertrue
4.125 +\def \mpr@htovlist {%
4.126 + \setbox \mpr@hlist
4.127 + \hbox {\strut
4.128 + \ifmpr@center \hskip -0.5\wd\mpr@hlist\fi
4.129 + \unhbox \mpr@hlist}%
4.130 + \setbox \mpr@vlist
4.131 + \vbox {\if@premisse \box \mpr@hlist \unvbox \mpr@vlist
4.132 + \else \unvbox \mpr@vlist \box \mpr@hlist
4.133 + \fi}%
4.134 +}
4.135 +% OLD version
4.136 +% \def \mpr@htovlist {%
4.137 +% \setbox \mpr@hlist
4.138 +% \hbox {\strut \hskip -0.5\wd\mpr@hlist \unhbox \mpr@hlist}%
4.139 +% \setbox \mpr@vlist
4.140 +% \vbox {\if@premisse \box \mpr@hlist \unvbox \mpr@vlist
4.141 +% \else \unvbox \mpr@vlist \box \mpr@hlist
4.142 +% \fi}%
4.143 +% }
4.144 +
4.145 +
4.146 +
4.147 +
4.148 +\def \mpr@blank { }
4.149 +\def \mpr@hovbox #1#2{\hbox
4.150 + \bgroup
4.151 + \ifx #1T\@premissetrue
4.152 + \else \ifx #1B\@premissefalse
4.153 + \else
4.154 + \PackageError{mathpartir}
4.155 + {Premisse orientation should either be P or B}
4.156 + {Fatal error in Package}%
4.157 + \fi \fi
4.158 + \def \@test {#2}\ifx \@test \mpr@blank\else
4.159 + \setbox \mpr@hlist \hbox {}%
4.160 + \setbox \mpr@vlist \vbox {}%
4.161 + \if@premisse \let \snoc \mpr@cons \else \let \snoc \mpr@snoc \fi
4.162 + \let \@hvlist \empty \let \@rev \empty
4.163 + \mpr@tmpdim 0em
4.164 + \expandafter \mpr@makelist #2\to \mpr@flat
4.165 + \if@premisse \mpr@rev \mpr@flat \to \@rev \else \let \@rev \mpr@flat \fi
4.166 + \def \\##1{%
4.167 + \def \@test {##1}\ifx \@test \empty
4.168 + \mpr@htovlist
4.169 + \mpr@tmpdim 0em %%% last bug fix not extensively checked
4.170 + \else
4.171 + \setbox0 \hbox{$\displaystyle {##1}$}\relax
4.172 + \advance \mpr@tmpdim by \wd0
4.173 + %\mpr@tmpdim 1.02\mpr@tmpdim
4.174 + \ifnum \mpr@tmpdim < \hsize
4.175 + \ifnum \wd\mpr@hlist > 0
4.176 + \if@premisse
4.177 + \setbox \mpr@hlist \hbox {\unhbox0 \qquad \unhbox \mpr@hlist}%
4.178 + \else
4.179 + \setbox \mpr@hlist \hbox {\unhbox \mpr@hlist \qquad \unhbox0}%
4.180 + \fi
4.181 + \else
4.182 + \setbox \mpr@hlist \hbox {\unhbox0}%
4.183 + \fi
4.184 + \else
4.185 + \ifnum \wd \mpr@hlist > 0
4.186 + \mpr@htovlist
4.187 + \mpr@tmpdim \wd0
4.188 + \fi
4.189 + \setbox \mpr@hlist \hbox {\unhbox0}%
4.190 + \fi
4.191 + \advance \mpr@tmpdim by 2em
4.192 + \fi
4.193 + }%
4.194 + \@rev
4.195 + \mpr@htovlist
4.196 + \ifmpr@center \hskip \wd\mpr@vlist\fi \box \mpr@vlist
4.197 + \fi
4.198 + \egroup
4.199 +}
4.200 +
4.201 +%%% INFERENCE RULES
4.202 +
4.203 +\@ifundefined{@@over}{%
4.204 + \let\@@over\over % fallback if amsmath is not loaded
4.205 + \let\@@overwithdelims\overwithdelims
4.206 + \let\@@atop\atop \let\@@atopwithdelims\atopwithdelims
4.207 + \let\@@above\above \let\@@abovewithdelims\abovewithdelims
4.208 + }{}
4.209 +
4.210 +
4.211 +\def \mpr@@fraction #1#2{\hbox {\advance \hsize by -0.5em
4.212 + $\displaystyle {#1\@@over #2}$}}
4.213 +\let \mpr@fraction \mpr@@fraction
4.214 +\def \mpr@@reduce #1#2{\hbox
4.215 + {$\lower 0.01pt \mpr@@fraction {#1}{#2}\mkern -15mu\rightarrow$}}
4.216 +\def \mpr@infercenter #1{\vcenter {\mpr@hovbox{T}{#1}}}
4.217 +
4.218 +\def \mpr@empty {}
4.219 +\def \mpr@inferrule
4.220 + {\bgroup
4.221 + \mpr@rulelineskip
4.222 + \let \and \qquad
4.223 + \let \hva \mpr@hva
4.224 + \let \@rulename \mpr@empty
4.225 + \let \@rule@options \mpr@empty
4.226 + \mpr@inferrule@}
4.227 +\newcommand {\mpr@inferrule@}[3][]
4.228 + {\everymath={\displaystyle}%
4.229 + \def \@test {#2}\ifx \empty \@test
4.230 + \setbox0 \hbox {$\vcenter {\mpr@hovbox{B}{#3}}$}%
4.231 + \else
4.232 + \def \@test {#3}\ifx \empty \@test
4.233 + \setbox0 \hbox {$\vcenter {\mpr@hovbox{T}{#2}}$}%
4.234 + \else
4.235 + \setbox0 \mpr@fraction {\mpr@hovbox{T}{#2}}{\mpr@hovbox{B}{#3}}%
4.236 + \fi \fi
4.237 + \def \@test {#1}\ifx \@test\empty \box0
4.238 + \else \vbox
4.239 +%%% Suggestion de Francois pour les etiquettes longues
4.240 +%%% {\hbox to \wd0 {\TirName {#1}\hfil}\box0}\fi
4.241 + {\hbox {\TirName {#1}}\box0}\fi
4.242 + \egroup}
4.243 +
4.244 +\def \mpr@vdotfil #1{\vbox to #1{\leaders \hbox{$\cdot$} \vfil}}
4.245 +
4.246 +% They are two forms
4.247 +% \mathrule [label]{[premisses}{conclusions}
4.248 +% or
4.249 +% \mathrule* [options]{[premisses}{conclusions}
4.250 +%
4.251 +% Premisses and conclusions are lists of elements separated by \\
4.252 +% Each \\ produces a break, attempting horizontal breaks if possible,
4.253 +% and vertical breaks if needed.
4.254 +%
4.255 +% An empty element obtained by \\\\ produces a vertical break in all cases.
4.256 +%
4.257 +% The former rule is aligned on the fraction bar.
4.258 +% The optional label appears on top of the rule
4.259 +% The second form to be used in a derivation tree is aligned on the last
4.260 +% line of its conclusion
4.261 +%
4.262 +% The second form can be parameterized, using the key=val interface. The
4.263 +% folloiwng keys are recognized:
4.264 +%
4.265 +% width set the width of the rule to val
4.266 +% narrower set the width of the rule to val\hsize
4.267 +% before execute val at the beginning/left
4.268 +% lab put a label [Val] on top of the rule
4.269 +% lskip add negative skip on the right
4.270 +% llab put a left label [Val], ignoring its width
4.271 +% left put a left label [Val]
4.272 +% right put a right label [Val]
4.273 +% rlab put a right label [Val], ignoring its width
4.274 +% rskip add negative skip on the left
4.275 +% vdots lift the rule by val and fill vertical space with dots
4.276 +% after execute val at the end/right
4.277 +%
4.278 +% Note that most options must come in this order to avoid strange
4.279 +% typesetting (in particular lskip must preceed left and llab and
4.280 +% rskip must follow rlab or right; vdots must come last or be followed by
4.281 +% rskip.
4.282 +%
4.283 +
4.284 +\define@key {mprset}{flushleft}[]{\mpr@centerfalse}
4.285 +\define@key {mprset}{center}[]{\mpr@centertrue}
4.286 +\def \mprset #1{\setkeys{mprset}{#1}}
4.287 +
4.288 +\newbox \mpr@right
4.289 +\define@key {mpr}{flushleft}[]{\mpr@centerfalse}
4.290 +\define@key {mpr}{center}[]{\mpr@centertrue}
4.291 +\define@key {mpr}{left}{\setbox0 \hbox {$\TirName {#1}\;$}\relax
4.292 + \advance \hsize by -\wd0\box0}
4.293 +\define@key {mpr}{width}{\hsize #1}
4.294 +\define@key {mpr}{before}{#1}
4.295 +\define@key {mpr}{lab}{\def \mpr@rulename {[#1]}}
4.296 +\define@key {mpr}{Lab}{\def \mpr@rulename {#1}}
4.297 +\define@key {mpr}{narrower}{\hsize #1\hsize}
4.298 +\define@key {mpr}{leftskip}{\hskip -#1}
4.299 +\define@key {mpr}{reduce}[]{\let \mpr@fraction \mpr@@reduce}
4.300 +\define@key {mpr}{rightskip}
4.301 + {\setbox \mpr@right \hbox {\unhbox \mpr@right \hskip -#1}}
4.302 +\define@key {mpr}{left}{\setbox0 \hbox {$\TirName {#1}\;$}\relax
4.303 + \advance \hsize by -\wd0\box0}
4.304 +\define@key {mpr}{Left}{\llap{$\TirName {#1}\;$}}
4.305 +\define@key {mpr}{right}
4.306 + {\setbox0 \hbox {$\;\TirName {#1}$}\relax \advance \hsize by -\wd0
4.307 + \setbox \mpr@right \hbox {\unhbox \mpr@right \unhbox0}}
4.308 +\define@key {mpr}{Right}
4.309 + {\setbox \mpr@right \hbox {\unhbox \mpr@right \rlap {$\;\TirName {#1}$}}}
4.310 +\define@key {mpr}{vdots}{\def \mpr@vdots {\@@atop \mpr@vdotfil{#1}}}
4.311 +\define@key {mpr}{after}{\edef \mpr@after {\mpr@after #1}}
4.312 +
4.313 +\newdimen \rule@dimen
4.314 +\newcommand \mpr@inferstar@ [3][]{\setbox0
4.315 + \hbox {\let \mpr@rulename \mpr@empty \let \mpr@vdots \relax
4.316 + \setbox \mpr@right \hbox{}%
4.317 + $\setkeys{mpr}{#1}%
4.318 + \ifx \mpr@rulename \mpr@empty \mpr@inferrule {#2}{#3}\else
4.319 + \mpr@inferrule [{\mpr@rulename}]{#2}{#3}\fi
4.320 + \box \mpr@right \mpr@vdots$}
4.321 + \setbox1 \hbox {\strut}
4.322 + \rule@dimen \dp0 \advance \rule@dimen by -\dp1
4.323 + \raise \rule@dimen \box0}
4.324 +
4.325 +\def \mpr@infer {\@ifnextchar *{\mpr@inferstar}{\mpr@inferrule}}
4.326 +\newcommand \mpr@err@skipargs[3][]{}
4.327 +\def \mpr@inferstar*{\ifmmode
4.328 + \let \@do \mpr@inferstar@
4.329 + \else
4.330 + \let \@do \mpr@err@skipargs
4.331 + \PackageError {mathpartir}
4.332 + {\string\inferrule* can only be used in math mode}{}%
4.333 + \fi \@do}
4.334 +
4.335 +
4.336 +%%% Exports
4.337 +
4.338 +% Envirnonment mathpar
4.339 +
4.340 +\let \inferrule \mpr@infer
4.341 +
4.342 +% make a short name \infer is not already defined
4.343 +\@ifundefined {infer}{\let \infer \mpr@infer}{}
4.344 +
4.345 +\def \tir@name #1{\hbox {\small \sc #1}}
4.346 +\let \TirName \tir@name
4.347 +
4.348 +%%% Other Exports
4.349 +
4.350 +% \let \listcons \mpr@cons
4.351 +% \let \listsnoc \mpr@snoc
4.352 +% \let \listhead \mpr@head
4.353 +% \let \listmake \mpr@makelist
4.354 +
4.355 +
4.356 +\endinput
4.357 +
5.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
5.2 +++ b/doc-src/LaTeXsugar/Sugar/document/root.tex Mon Nov 29 11:12:19 2004 +0100
5.3 @@ -0,0 +1,59 @@
5.4 +\documentclass[11pt,a4paper]{article}
5.5 +\usepackage{isabelle,isabellesym}
5.6 +
5.7 +% further packages required for unusual symbols (see also isabellesym.sty)
5.8 +% use only when needed
5.9 +%\usepackage{amssymb} % for \<leadsto>, \<box>, \<diamond>,
5.10 + % \<sqsupset>, \<mho>, \<Join>,
5.11 + % \<lhd>, \<lesssim>, \<greatersim>,
5.12 + % \<lessapprox>, \<greaterapprox>,
5.13 + % \<triangleq>, \<yen>, \<lozenge>
5.14 +%\usepackage[greek,english]{babel} % greek for \<euro>,
5.15 + % english for \<guillemotleft>,
5.16 + % \<guillemotright>
5.17 + % default language = last
5.18 +%\usepackage[latin1]{inputenc} % for \<onesuperior>, \<onequarter>,
5.19 + % \<twosuperior>, \<onehalf>,
5.20 + % \<threesuperior>, \<threequarters>,
5.21 + % \<degree>
5.22 +%\usepackage[only,bigsqcap]{stmaryrd} % for \<Sqinter>
5.23 +%\usepackage{eufrak} % for \<AA> ... \<ZZ>, \<aa> ... \<zz>
5.24 + % (only needed if amssymb not used)
5.25 +%\usepackage{textcomp} % for \<cent>, \<currency>
5.26 +
5.27 +\usepackage{mathpartir}
5.28 +
5.29 +% this should be the last package used
5.30 +\usepackage{pdfsetup}
5.31 +
5.32 +% urls in roman style, theory text in math-similar italics
5.33 +\urlstyle{rm}
5.34 +\isabellestyle{it}
5.35 +
5.36 +
5.37 +\begin{document}
5.38 +
5.39 +\title{\LaTeX\ Sugar for Isabelle/HOL}
5.40 +\author{Tobias Nipkow, Norbert Schirmer}
5.41 +\maketitle
5.42 +
5.43 +\begin{abstract}
5.44 +This document shows you how to typset mathematics in Isabelle-based
5.45 +documents in a style close to that in ordinary computer science papers.
5.46 +\end{abstract}
5.47 +
5.48 +\tableofcontents
5.49 +
5.50 +% generated text of all theories
5.51 +\input{session}
5.52 +
5.53 +% optional bibliography
5.54 +%\bibliographystyle{abbrv}
5.55 +%\bibliography{root}
5.56 +
5.57 +\end{document}
5.58 +
5.59 +%%% Local Variables:
5.60 +%%% mode: latex
5.61 +%%% TeX-master: t
5.62 +%%% End: