"Fossies" - the Fresh Open Source Software Archive

Member "hevea-2.35/examples/pat.def" (16 Jan 2021, 21990 Bytes) of package /linux/www/hevea-2.35.tar.gz:


As a special service "Fossies" has tried to format the requested source page into HTML format using (guessed) Modula2 source code syntax highlighting (style: standard) with prefixed line numbers. Alternatively you can here view or download the uninterpreted source code file.

    1 \makeatletter
    2 
    3 \typeout{``page''}
    4 
    5 % cedric: removed for llncs
    6 
    7 %page layout
    8 %\oddsidemargin 0cm
    9 %\evensidemargin 0cm
   10 %\topmargin 10pt
   11 
   12 %\headheight 0pt    
   13 %\headsep 0pt   
   14 %\footheight 0pt
   15 %\footskip 24pt 
   16 %\textheight 24cm
   17 %\textwidth 15.5cm
   18 %\footnotesep 1cm
   19 
   20 %\baselineskip = 24pt plus 4pt minus 3pt
   21 %\voffset=-0.5cm
   22 %\hoffset=0.5cm
   23 
   24 \makeatother
   25 
   26 \makeatletter
   27 
   28 % on  active  et  desactive  le  mode  frtypo  par \frtypotrue et frtypofalse
   29 % quelquesoit le mode les caract\`eres :  ; ?   !   sont actifs. 
   30 % En  particulier  ces  caract\`eres  ne  peuvent  plus \^etre  mis  dans des
   31 % \'etiquettes.
   32 
   33 \def\halfspace{\kern .166em}
   34 
   35 \def\space@pv{\ifmmode ;\else \halfspace;\fi}
   36 \def\space@dc{\ifmmode :\else \halfspace:\fi}
   37 \def\space@pi{\ifmmode ?\else \halfspace?\fi}
   38 \def\space@pe{\ifmmode !\else \halfspace!\fi}
   39 
   40 \let\nospace@pv=;
   41 \let\nospace@dc=:
   42 \let\nospace@pi=?
   43 \let\nospace@pe=!
   44 
   45 \catcode`;=\active \catcode`:=\active \catcode`?=\active \catcode`!=\active
   46 
   47 \def \frtypo
   48     {\let;=\space@pv\let:=\space@dc\let!=\space@pe\let?=\space@pi}
   49 \def \entypo 
   50     {\let;=\nospace@pv\let:=\nospace@dc\let!=\nospace@pe\let?=\nospace@pi}
   51 
   52 \frtypo
   53 
   54 \def\@sanitize
   55  {\@makeother\ \@makeother\\\@makeother\$\@makeother\&%
   56 \@makeother\#\@makeother\^\@makeother\^^K\@makeother\_\@makeother\^^A%
   57 \@makeother\%\@makeother\~\@makeother\;\@makeother\?\@makeother%
   58 \:\@makeother\!}
   59 
   60 \let \oldspecials \dospecials 
   61 \def \dospecials {\oldspecials \do\:\do\!\do \?\do\;}
   62 
   63 %\scrollmode
   64 
   65 \makeatletter
   66 %===========================================================================
   67 % Personals macros (They might have strange latex side effects
   68 %-----------------
   69 
   70 \def\noparindent{\everypar={\hskip -\parindent\everypar={}}}
   71 \def \para {\medskip\noparindent}
   72 \def \pari {\medskip\noparindent}
   73 \def \parii {\smallskip\noparindent}
   74 \let\paro=\noparindent
   75 
   76 
   77 %===========================================================================
   78 % Definitions Theorems 
   79 %---------------------
   80 
   81 \newif \iffrench 
   82 \if \csname french\endcsname \relax  \frenchfalse \else  \frenchtrue\fi
   83 
   84 \if \csname definition\endcsname\relax
   85 \newtheorem{definition}{D\iffrench \'e\else e\fi  finition}\fi
   86 \def\bdf{\begin{definition}\begin{em}}
   87 \def\edf{\ifvmode\vskip-\lastskip\nopagebreak\else
   88          \penalty 100\fi\end{em}\end{definition}}
   89 
   90 \if \csname theorem\endcsname\relax
   91 \newtheorem{theorem}{\iffrench Théorème\else Theorem\fi}\fi
   92 \def\bthm{\begin{theorem}}
   93 \def\ethm{\end{theorem}}
   94 
   95 \newtheorem{algorithm}{Algorithm\if\french e\else\fi}
   96 \def\balgo{\begin{algorithm}}
   97 \def\ealgo{\end{algorithm}}
   98 
   99 \if \csname proposition\endcsname\relax
  100 \newtheorem{proposition}{Proposition}\fi
  101 \def\bprop{\begin{proposition}}
  102 \def\eprop{\end{proposition}}
  103 
  104 \if \csname lemma\endcsname\relax 
  105 \newtheorem{lemma}[proposition]{Lemm\iffrench e\else a\fi}\fi
  106 \def\blem{\begin{lemma}}
  107 \def\elem{\end{lemma}}
  108 
  109 \if \csname corollary\endcsname\relax
  110 \newtheorem{corollary}[proposition]{Corollary}\fi
  111 \def\bcor{\begin{corollary}}
  112 \def\ecor{\end{corollary}}
  113 
  114 \def\brmk{\trivlist \item[\hskip \labelsep {\bf {Note}}]}
  115 \def\ermk{\endtrivlist}
  116 
  117 \newtheorem{Note}{Note}
  118 \def\bnote{\begin{note}\begin{em}}
  119 \def\enote{\end{em}\end{note}}
  120 
  121 \if \csname example\endcsname\relax
  122 %\newtheorem{example}[remark]{Ex\iffrench a\else e\fi mple}\fi
  123 \newtheorem{example}{Ex\iffrench a\else e\fi mple}\fi
  124 \def\bxple{\trivlist \item[\hskip \labelsep {\bf {Example}}]}
  125 %{\begin{example}\begin{em}}
  126 \def\exple{\endtrivlist}
  127 %{\end{em}\end{example}}
  128 
  129 \def\@begintheorem#1#2{\it \trivlist \item[\hskip \labelsep{\bf #1\ #2}]}
  130 \def\@opargbegintheorem#1#2#3{\it \trivlist
  131       \item[\hskip \labelsep{\bf #1\ #2\ (#3)}]}
  132 \def\@endtheorem{\endtrivlist}
  133 
  134 \newcount \indemo
  135 \def \makeno #1{\global \advance \indemo by 1\global
  136       \expandafter \edef \csname demo/\the\cdemo/#1\endcsname{\the\indemo}}
  137 \def \refno #1{\if \relax\csname demo/\the\cdemo/#1\endcsname \relax
  138   \write0 {Demo counter #1 undefined}??\else
  139    \csname demo/\the\cdemo/#1\endcsname\fi}
  140 \def \labno #1{\makeno {#1}\refno {#1}}
  141 
  142 \newif \ifdemo \demotrue
  143 \newcount \cdemo
  144 \newenvironment{demo}{\bdemo}{\edemo}
  145 \def\bdemotrue{\trivlist \item[\hskip \labelsep
  146   {\underline
  147         {\iffrench Preuve\else Proof\fi}:}]\advance\cdemo by 1\indemo 0}
  148 \def\edemo{\penalty 100\hfill\rule{2mm}{2mm} \endtrivlist\@doendpe}
  149 \long \def \bdemofalse #1\edemo{\relax}
  150 \outer \def \bdemo 
  151   {\ifdemo \bdemotrue \else \expandafter \bdemofalse \fi\indent}
  152 
  153 \newif \ifhint \hintfalse
  154 \newtheorem{hint}{\rm \underline {Hint}}
  155 \def\bhintiftrue{\trivlist \item[\hskip \labelsep {\underline {Hint}:}]}
  156 \def\ehint{\penalty 100\hfill\noindent\rule{2mm}{2mm}\endtrivlist}
  157 \long \def \bhintiffalse #1\ehint{\relax}
  158 \outer \def \bhint
  159   {\ifhint \bhintiftrue \else \expandafter \bhintiffalse \fi}
  160 
  161 \newif \ifexpert \expertfalse
  162 \newtheorem{expert}{Remark}
  163 \def\bexpertiftrue{\trivlist \item[\hskip \labelsep {\underline {Hint}:}]}
  164 \def\eexpert{\penalty 100\hfill\noindent\rule{2mm}{2mm}\endtrivlist}
  165 \long \def \bexpertiffalse #1\eexpert{\relax}
  166 \outer \def \bexpert 
  167   {\ifexpert \bexpertiftrue \else  \expandafter \bexpertiffalse \fi}
  168 
  169 
  170 
  171 \def\notitle{\hskip\hsize minus\hsize\nobreak\hbox{}}
  172 
  173 \def\notation{\paragraph*{Notation}}
  174 \def\hypothesis{\paragraph*{Assumption}}
  175 
  176 
  177 \def \caseparagraph{\@startsection
  178  {case}{6}{\z@}{1.5ex plus .3ex minus .2ex}{-1em}{\normalsize\bf}}
  179 \def \subcaseparagraph{\@startsection
  180 % {subcase}{7}{\parindent}{1.5ex plus .3ex minus .2ex}{-1em}{\normalsize\bf}}
  181  {subcase}{7}{\z@}{1.5ex plus .3ex minus .2ex}{-1em}{\normalsize\bf}}
  182 
  183 
  184 \if \csname datefrench\endcsname\relax
  185 \def \langcase {Case}
  186 \def \langsubcase {Subcase}
  187 \else
  188 \def \langcase {Cas}
  189 \def \langsubcase {Sous-cas}
  190 \fi
  191 
  192 \def\case#1{\caseparagraph*{\langcase\space #1:}}
  193 \def\othercase#1{\caseparagraph*{#1:}}
  194 \def\mathcase#1{\caseparagraph*{\langcase\space $#1$:}}
  195 \def\subcase#1{\subcaseparagraph*{\langsubcase\space #1:}}
  196 
  197 % Send a warning when running latex
  198 \def\warning#1{\immediate\write0{Warning: #1}}
  199 
  200 \newenvironment{care}{\bwarning}{\ewarning}
  201 \def\bcare{\trivlist \item[\hskip \labelsep {\bf Warning!}]}
  202 \def\ecare{\endtrivlist}
  203 
  204 \def\subst#1#2{^{#1} \!/\! _{#2}}
  205 
  206 \def \comment #1{{\em #1}}
  207 %\def \comment #1{}
  208 \makeatother
  209 
  210 
  211 \makeatletter
  212 %%% To change size in math mode
  213 
  214 \let\Ts=\textstyle
  215 \let\Ds=\displaystyle
  216 \let\Ss=\scriptstyle
  217 
  218 %%% Abrevs
  219 
  220 \let \comp \circ
  221 \let \wild \_
  222 
  223 
  224 %%% To put text between two formulas on the same line
  225 
  226 \def\text#1{\qquad\hbox{#1}\qquad}
  227 
  228 %%%  Macros for mathematics
  229 
  230 %% Special symbols
  231 
  232 \def \nat {{\mathord{I\kern -.33em N}}}
  233 \def \natb {{\mathord{I\kern -.33em\overline{N}}}}
  234 
  235 \def\Vdash {\mathrel{\hbox{\vrule\kern .1ex$\vdash$}}}
  236 \def\VVdash {\mathrel{\hbox{\vrule\kern .2ex\vrule\kern .1ex $\vdash$}}}
  237 
  238 % An open box to end demonstrations with
  239 
  240 \def\Box{\hbox
  241   {\vbox
  242     {\hrule height .033em
  243      \hbox to .5em
  244        {\vrule width .033em
  245         \hbox{\vbox to .5em{\vss}\hss}
  246         \vrule width .033em}
  247      \hrule height .033em
  248     }}}
  249 
  250 
  251 %% Balanced symbols
  252 
  253 \def\absolute#1{\mathopen\mid#1\mathclose\mid}
  254 
  255 %% Operators
  256 
  257 \def \domain {\dv}
  258 %\def \domain {\dvmathop{\sl dom\,}}
  259 \def \image {\mathop{\sl im\,}}
  260 \def \modulo {\mathbin{\rm modulo}}
  261 \def \inverse{{}^{-1}}
  262 \def \cardinal {{\sl Card\,}}
  263 %\def \restrict #1{\mathbin{\mid}_{#1}}
  264 \def \restrict
  265    {\mathbin{\hbox{$\mid$\kern-.24em\lower.09em\hbox{\rm\char'22}$\!$}}}
  266 \let \arity = \varrho
  267 
  268 
  269 %% Quantifiers
  270 
  271 \def \fall #1,{\forall #1,\;}
  272 \def \exist #1,{\exists #1,\;}
  273 \def \qt #1.{\forall\,#1.\,}
  274 \def \ex #1.{\exists\,#1.\,}
  275 
  276 %% Arrows
  277 
  278 \let\ar=\rightarrow
  279 \let\dar=\Rightarrow
  280 \def\imply{\Longrightarrow}
  281 
  282 
  283 \def \rewrite {\mathrel{-}\joinrel\leadsto}
  284 
  285 
  286 %% Equalities
  287 
  288 %\def \axiom {\mathrel {\mathop =^!}}
  289 \def \axiom {=}
  290 \def \eqdef {\mathrel {\mathop {=\joinrel=}\limits^{def}}}
  291 
  292 %% Sizes
  293 
  294 \def\({\left(}
  295 \def\){\right)}
  296 
  297 \def\Mid{\mathrel{\Big|}}
  298 
  299 %% Indices  see also indices.def
  300 
  301 \def \ind #1#2{_{#1\in[1,#2]}}
  302 
  303 %%
  304 
  305 %% names 
  306 
  307 \let \th \vdash
  308 \let \tth \Vdash
  309 \let \ttth \VVdash
  310 \let \thh \models
  311 
  312 \def\Cal#1{{\cal #1}}
  313 
  314 \let \eset = \emptyset
  315 
  316 
  317 
  318 %% Aligned constructions in math mode
  319 
  320 % For internal use only
  321 
  322 \def\noskip{\lineskiplimit=\the\lineskiplimit
  323                 \lineskip=\the\lineskip}
  324 \def\moreskip{\lineskiplimit=0.4em\lineskip=0.4em plus 0.2em}
  325 \def\moremoreskip{\lineskiplimit=1.2em\lineskip=1.2em plus 0.2em}
  326 
  327 \def\vatrix#1{\null\,\vcenter{\normalbaselines\moreskip\m@th
  328     \let \and \cr
  329     \ialign{$\displaystyle##$\hfil
  330       &\quad$\displaystyle##$\hfil&\quad##\hfil\crcr
  331       \mathstrut\crcr\noalign{\kern-\baselineskip}
  332       #1\crcr\mathstrut\crcr\noalign{\kern-\baselineskip}}}\,}
  333 
  334 % A sequence of expressions is writen on separate lines to form one expression
  335 
  336 \def \band #1{\left\{\vatrix{#1}\right.}          % brace and
  337 \def \wand #1{\wedge\band{#1}}                    % wedge  and
  338 \def \vand #1{\vee\band{#1}}                      % vee  and
  339 \def \vor  #1{\vee\left[\vatrix{#1}\right.}       % vee and or
  340 \def \Wand #1{\bigwedge\band{#1}}                 % big wedge and
  341 \def \Vand #1{\bigvee\band{#1}}                   % big vee and
  342 \def \Wor  #1{\bigvee\left[\vatrix{#1}\right.}    % big vee and
  343 
  344 
  345 
  346 % A general usage tabulation in math mode.
  347 %     Indentation is alternatively left and right, so that good place for
  348 %     tabs will produce many different
  349 
  350 % \dalign { & blabla :& blabla    \cr 
  351 %           &    bla :& blablabla \cr
  352 %         }
  353  
  354 % \dalign {  blabla :&& blabla    \cr 
  355 %            bla :   && blablabla \cr
  356 %         }
  357  
  358 % \dalign { & blabla :&    blabla \cr 
  359 %           &    bla :& blablabla \cr
  360 %         }
  361 
  362 % Internal and personal use
  363 \def\Dalign#1#2{\vcenter
  364  \bgroup
  365    \let\>=\qquad
  366    \def\title##1{\crcr\noalign{\medskip}\multispan#1{\hfil\bf##1\hfil}}
  367 %   \halign{$##$\hfil\qquad&&\hfil$##{}$&${}##$\hfil\qquad\cr#2\crcr}
  368 %   \halign{$##$\hfil&&\qquad\hfil$##{}$&${}##$\hfil\cr#2\crcr}
  369    \halign{&${}##$\hfil&\hfil$##{}$\cr#2\crcr}
  370  \egroup}
  371 % End internal use
  372 
  373 \def\align#1{\vcenter
  374  \bgroup
  375    \let\>=\qquad
  376    \halign{#1\crcr}
  377  \egroup}
  378 
  379 %\def\aligndef#1#2{\expandafter\def\csname aligndef#1\endcsname{#2}}
  380 %\aligndef ]{\argalign}
  381 %\aligndef l{&\hfil$##{}$}
  382 %\aligndef r{&${}##$\hfil}
  383 %\aligndef c{&\hfil$##$\hfil}
  384 %\aligndef -{\qquad}
  385 %\aligndef L{&\hfil##$}
  386 %\aligndef R{&##\hfil}
  387 %\aligndef C{&\hfil##\hfil}
  388 %\def\argalign#1{\relax}
  389 %\def\prealign#1{\csname aligndef#1\endcsname\prealign}
  390 %\def\doalign#1]{\dohalign{\prealign#1]}}
  391 %\def\dohalign#1#2{\expandafter\halign{#1\cr#2\crcr}}
  392 
  393 
  394 
  395 %\def\dalign#1{\ifx#1[\doalign\else\Dalign3{#1}\fi}
  396 \def\dalign{\Dalign3}
  397 
  398 
  399 \def\Strut{\raise .4em\hbox{\strut}\raise -.4em\hbox{\strut}}
  400 
  401 \def \deftitle #1
  402    {\def \title ##1
  403       {\crcr\noalign{\medskip}\multispan#1{\hfil\bf##1\hfil}}}
  404 
  405 
  406 
  407 \bgroup
  408  \catcode `\^^M \active
  409  \gdef \obeycr {\catcode `\^^M\active \let ^^M\crcr}
  410 \egroup
  411 
  412 
  413 \ifx \csname linewidth\endcsname \hsize 
  414  \let  \realwidth \hsize 
  415 \else
  416  \let \realwidth \linewidth
  417 \fi
  418 
  419 \def \oris {\crcr \mid&}
  420 \def \syntaxtable #1
  421   {\def\is {::=&}
  422    \def \\{\cr\noalign{\medskip}}\def\cont{\cr&}\vbox 
  423    \bgroup
  424    \tabskip=100pt plus 1000pt minus 1000pt
  425    \halign to \realwidth
  426        {\hfil$##{}$\tabskip=0pt&
  427         ${}##$\hfil \tabskip=100pt plus 1000pt minus 1000pt&
  428         &##\hfil \cr#1\crcr}
  429    \egroup}
  430 
  431 
  432 \def \assertions #1
  433   {\deftitle2 \vbox
  434    \bgroup
  435      \halign {\hfil$##{}$&$##$\hfil&&\quad##\hfil\cr#1\crcr}
  436    \egroup}
  437 
  438 
  439 %%% old version
  440 
  441 \def\malign#1{\vcenter\bgroup
  442    \deftitle #1
  443    \def \lign ##1\cr {\noalign {##1}}
  444    \def \textlign##1{\noalign {\medskip \vbox {\noindent ##1}\medskip}}
  445    \tabskip=100pt plus 1000pt minus 1000pt
  446    \halign to \realwidth
  447        {\hfil$##{}$\tabskip=0pt&
  448         ${}##$\hfil \tabskip=100pt plus 1000pt minus 1000pt&
  449         &##\hfil&$##$\hfil&  \cr#1\crcr\egroup}}
  450 
  451 \newif \ifhsize \hsizefalse
  452 
  453 \newskip \nullskip \nullskip 0pt
  454 \newskip \fullskip \fullskip 100pt plus 1000pt minus 1000pt
  455 \def \maligntrue {\tabskip \fullskip
  456                    \halign to \realwidth \bgroup}
  457 \def \malignfalse {\halign \bgroup}
  458 \def \malign {\vcenter \bgroup \ifhsize \expandafter \maligntrue \else \expandafter \malignfalse \fi}
  459 \def \endmalign {\crcr \egroup \egroup}
  460 
  461 \def \makeword #1#2#3{\expandafter
  462    \def \noexpand#3{#2 {#1\expandafter \let \expandafter \dummy\string #3}}}
  463 
  464 \let \vect \overrightarrow
  465 
  466 \def \uad {\hskip 0.5em}
  467 
  468 
  469 \newskip \mathandskip 
  470 \newskip\mathmargin \mathmargin  0em
  471 
  472 \mathandskip 2em plus 0.5fil minus 0.5em
  473 \def \mathand {\hskip \mathandskip}
  474 \def \mathleftright {\hfill{}\hskip 0em plus -2fill\penalty 50{}\hfill}
  475 \def \mathandcr {\penalty 50\mathand}
  476 \def \mathcr {\penalty -10000\mathand}
  477 \def \mathcrleft {\hfill{}\hskip 0em plus -2fill\penalty -10000{}\hskip
  478      \mathmargin}
  479 \def \mathbreak {\penalty 50}
  480 
  481 \def \incrmargin #1{\advance\mathmargin by #1em\advance\mathmargin by #1em}
  482 \def \mathslash#1{\let \do \mathcrleft
  483    \ifx #1[\let\do\mathdoskip\fi\do#1}
  484 \def \mathdoskip#1#2]{\incrmargin {#2}\mathcrleft}
  485 
  486 % Type inference rules
  487 
  488 \let \mathmoreskip=\moremoreskip
  489 \def \nomoreskip {\let \mathmoreskip \relax}
  490 
  491 \def \bmaths {\let \and \mathandcr  \hsize \realwidth
  492     \centering \vbox \bgroup \mathmoreskip  \noindent 
  493     $\displaystyle \let \\ \mathslash}
  494 \def \emaths {\unskip$\egroup}
  495 \def \mathflushleft {\def \emaths {\hfill$\egroup}\nomoreskip}
  496 \newenvironment {maths}{\bmaths}{\emaths}
  497 
  498 \def \maths #1{\bmaths #1\emaths}
  499 
  500 \def \whereis {\leftarrow}
  501 \def \where #1{[{\let \is \whereis #1}]}
  502 \def \dowhere #1\is#2\is{[\ifx#2\empty #1\else #2/#1\fi]}
  503 \def \where #1{\let \is \relax\dowhere #1\is\empty\is}
  504 
  505 \let \closeplus\relax
  506 \let \Empty \relax
  507 \let \is \relax
  508 \def \plus #1{\PLUS #1\is\is\END}
  509 \def \PLUS #1\is#2\is#3\END{\oplus\ifx #3\is (#1\plustoken#2)\else #1\fi}
  510 \let \plustoken \mapsto
  511 
  512 \let \diverge \uparrow
  513 
  514 \def \set #1{\{#1\}}
  515 \def \sem #1{\lbrack\!\lbrack#1\rbrack\!\rbrack}
  516 
  517 
  518 \def\mathrm #1{\mathrel {\rm #1}}
  519 \let \coerce \leq
  520 \makeatother
  521 
  522 \makeatletter
  523 
  524 
  525 %% see infer.doc for a documentation
  526 
  527 % Judgements
  528 
  529 \let\th=\vdash
  530 
  531 % naming
  532 
  533 \expandafter \ifx \csname name\endcsname\relax
  534    \def\name#1{\hbox{\sc #1}}\else \relax \fi
  535 
  536 \def \labname #1{{\rm(\name{#1})}}
  537 \let \lab = \labname
  538 \def \clab #1{\hbox {$\smash {\lab{#1}}$}}
  539 \newskip \beforelabskip \beforelabskip = 0.5em
  540 \def \eqlab {\eqno \lab}
  541 
  542 %% inside rules
  543 
  544 \def \nmir #1[#2]{\crcr \hrulefill \cr}
  545 \def \rmir #1[#2]{\crcr \hrulefill & \clab {#2} \cr}
  546 \def \lmir #1[#2]{\relax}                         
  547 \def \Lmir #1[#2]{\crcr \Llabo {#2}\hrulefill \cr}     
  548 \def \Rmir #1[#2]{\crcr \hrulefill \Rlabo {#2}\cr}    
  549 \def \imir {\crcr \hrulefill\cr}
  550 
  551 % outside rules
  552 
  553 \def \rlabo #1{\hskip \beforelabskip \clab {#1}} 
  554 \def \llabo #1{\clab {#1}\hskip \beforelabskip}
  555 \def \Rlabo #1{\rlap {\rlabo {#1}}}   
  556 \def \Llabo #1{\llap {\llabo {#1}}}   
  557 \let \labr \rlabo \let \labl \llabo \let \labR \Rlabo \let \labL \Llabo
  558 
  559 
  560 \def \rlab #1 {\rlap {\lab {#1}}}
  561 \def \llab #1 {\llap {\lab {#1}}}
  562 
  563 
  564 % A good separator for multiple hypothesis
  565 
  566 \let \and \qquad
  567 \let \andcr \cr
  568 
  569 
  570 % Single rules
  571 
  572 \def \lessskip  {\lineskiplimit=.3em\lineskip= .2em plus .1em}
  573 
  574 \makeatletter
  575 \def \mathrulename {\scriptsize \labname}
  576 \def \ignoredash #1{\let\next\ignoredash
  577          \ifx #1-\relax\else\let\next#1\fi\next}
  578 \def \mathrule {\@ifnextchar [{\mathrulelab}{\@mathrule}}
  579 \def \mathrulelab[#1]#2{\hbox
  580    {\vbox {\hbox {\mathrulename {#1}}\nointerlineskip\smallskip
  581            \hbox {$\@mathrule{#2}$}}}}
  582 \def \@mathrule #1{{\let \and \qquad \let \rlab \rl \let \llab \ll
  583      \def \mir {MiR}\def\endrule {EnDrUlE}
  584      \displaystyle \offinterlineskip \lessskip  \bgroup \openrule 
  585      \beginrule #1\mir \mir \endrule}}
  586 \def \beginrule #1\mir#2{#1\ifx #2\mir \let \next \finishrule 
  587      \else \def \next {\middlerule\openrule \beginrule\ignoredash#2}\fi\next} 
  588 \def\finishrule#1\endrule{\closerule\egroup}
  589 
  590 \def \openrule {\hbox \bgroup \vbox \bgroup
  591      \halign \bgroup \hfil $##$\hfil &\hskip \beforelabskip$##$\hfil \cr}
  592 \def \closerule {\crcr\egroup\egroup\egroup}
  593 %\def \endrule {\closerule \egroup}
  594 
  595 \def \singleRule {\crcr\noalign {\vskip -0.1em}\closerule \over}
  596 \let \middlerule \singleRule
  597 
  598 
  599 % Double and Tripple rules see infer-more.def
  600 
  601 % Logic and rewriterules
  602 
  603 \def \logicrule #1{\let \mir \Longrightarrow #1}
  604 
  605 
  606 \def \longleadsto {\mathrel{-}\joinrel\leadsto}
  607 
  608 \def \rewriterule #1{\displaystyle \offinterlineskip \lessskip
  609      \bgroup\let \mir \longleadsto \openrule#1\endrule}
  610 
  611 \def \suspend #1{\vbox to #1 {\leaders \hbox {$\cdot$}\vfill}}
  612 
  613 
  614 \if \relax \csname keywordstyle\endcsname  \let \keywordstyle \tt \fi
  615 
  616 %\def \keyword #1{{\hbox {\keywordstyle #1}}}
  617 \def \keyword #1{{\keywordstyle #1}}
  618 \def \mathtoken #1{\ifmmode
  619    \mathopen{}\keyword {#1}\mathclose{}\else \keyword{#1}\fi}
  620 \def \mathpostfix #1{\mathrel{\keyword {#1}}\mathclose{}}
  621 \def \mathprefix #1{\mathopen{}\mathrel{\keyword {#1}}}
  622 \def \mathinfix #1{\mathrel{\keyword {#1}}}
  623 
  624 \def\ignorefirst #1{}
  625 \def \lwt #1{\expandafter \lowercase \expandafter \bgroup 
  626   \expandafter \ignorefirst \string #1\egroup}
  627 
  628 
  629 \def \makeprefix #1#2{\expandafter\def \noexpand #1{\mathprefix  {#2}}}
  630 \def \makepostfix #1#2{\expandafter\def \noexpand #1{\mathpostfix  {#2}}}
  631 \def \maketoken #1#2{\expandafter\def \noexpand #1{\mathtoken {#2}}}
  632 \def \makeinfix #1#2{\expandafter\def \noexpand #1{\mathinfix {#2}}}
  633 
  634 \def \makein #1{\expandafter\def
  635   \noexpand #1##1in{\keyword {\lwt #1}\,\,##1\,\,\keyword {in}\,\,}}
  636 
  637 \let \@ \;
  638 \def \Let #1=#2in{\keyword {let}\@ {#1 = #2} \@\keyword {in}\@}
  639 \def \fun (#1){\keyword {fun}\@ #1 \rightarrow}
  640 \def \type #1=#2in{\keyword {type}\@ #1 = #2 \@\keyword {in}\@}
  641 
  642 \makeatother
  643 
  644 \let \cont \kappa
  645 \let \t \tau
  646 \let \l \ell
  647 \let \s \sigma
  648 \let \tv \alpha
  649 \let \vect \bar
  650 
  651 \def \Gen {{\rm Gen}}
  652 
  653 \def \tplus #1{\TPLUS #1\is\is\END}
  654 \def \TPLUS #1\is#2\is#3\END{\oplus\ifx #3\is (#1:#2)\else #1\fi}
  655 
  656 %%%%%%%%%%%%%%% light programs
  657 
  658 \makeatletter
  659 \def \progstyle {\tt}
  660 \newskip \programindent \programindent 4em
  661 \def \program {\par \begingroup 
  662     \medskip \parindent \programindent \@tempswafalse
  663     \frenchspacing \@vobeyspaces \let \par \programpar
  664     \obeylines \progstyle
  665     \catcode``=13 \@noligs \let \do \@makeother \dospecials 
  666     \catcode `\\ 0 \catcode `\{ 1 \catcode `\} 2
  667     \prog@specials \prog@initspecials \obeyspaces}
  668 
  669 \def \programpar {\if@tempswa\hbox{}\fi\@tempswatrue\@@par}
  670 
  671 \bgroup
  672 \gdef \less@specials {\relax
  673  \catcode `| \active 
  674  \catcode `< \active
  675  \catcode `> \active
  676  \catcode `- \active
  677  \catcode `\' \active 
  678 }
  679 \gdef \more@specials {\relax
  680  \catcode `( \active
  681  \catcode `) \active
  682 }
  683 \gdef \prog@specials {\less@specials\more@specials}
  684 \prog@specials
  685 \gdef \prog@initspecials {\def
  686     -{\minus@program}\def
  687     '{\acurate@program}\def
  688     |{\bar@program}\def
  689     <{\less@program}\def
  690     >{\greater@program}\def
  691     ({\less@program}\def
  692     ){\greater@program}}
  693  \gdef \bar@@program {\let\do \eattoken
  694   \ifx \token >$\droite$\else ${}\mid{}$\let \do \relax\fi \do}
  695  \gdef \minus@@program {\let\do \eattoken
  696   \ifx \token >$\ar$\else -\let \do \relax\fi \do}
  697 \egroup
  698 
  699 \def \acurate@program {\futurelet \token \acurate@@program}
  700 \def \acurate@@program {\let \do \eattoken
  701   \ifx \token a$\alpha$\else 
  702    \ifx \token b$\beta$\else 
  703     \char `\' \let \do \relax\fi\fi \do}
  704 \def \less@program {\hbox{$<$}}
  705 \def \greater@program {\hbox{$>$}}
  706 \def \bar@program {\futurelet \token \bar@@program}
  707 \def \minus@program {\futurelet \token \minus@@program}
  708 
  709 
  710 \def \endprogram {\ifdim\lastskip >\z@ \@tempskipa\lastskip 
  711        \vskip -\lastskip\fi\medskip \endgroup
  712      \@endpetrue}
  713 
  714 \def\prog {\begingroup \hbox \bgroup
  715   \catcode ``=13 \@noligs
  716   \let \do \@makeother \dospecials \progstyle
  717    \prog@specials \prog@initspecials
  718     \catcode `\\ 0 \catcode `\{ 1 \catcode `\} 2
  719   \@prog}
  720 \def\@prog#1{\obeyspaces \frenchspacing \catcode `\  10
  721             \def\@tempa ##1#1{##1\egroup\endgroup}\@tempa}
  722 \makeatother
  723 
  724 %%%%%%%%%%%%%%%%%%%  "quotations"
  725 
  726 \makeatletter
  727 % on  active  le cararectere " et on s'en sert pour le mode \prog
  728 % s'il est défini ou \verb autrement
  729 
  730 \bgroup
  731 \@makeother \"
  732 \gdef \progquote {\prog"}
  733 \catcode `\" \active
  734 \gdef "{\progquote}
  735 \egroup
  736 
  737 \def \quoteon {
  738 \let \quote@sanitize \@sanitize
  739 \def \@sanitize {\quote@sanitize \@makeother\"}
  740 \let \quote@specials \dospecials 
  741 \def \dospecials {\quote@specials \do\"}
  742 \def \quoteon {\catcode `\" \active}\quoteon}
  743 
  744 \def \quoteoff {\@makeother \"}
  745 \makeatother
  746 
  747 
  748 
  749 %%%%%%%%%%%%%%%%
  750 \def \lift #1{\;{}^{#1}}
  751 \def \inu #1{\lift {i \in 1..#1}}
  752 \def \jnu #1{\lift {j \in 1..#1}}
  753 
  754 %% typo
  755 
  756 \mathchardef \le "313C
  757 \mathchardef \ge "313E
  758 
  759 \mathcode `< "4268
  760 \mathcode `> "5269
  761 
  762 
  763 \catcode `\| \active 
  764 \let \olspecials \dospecials \def \dospecials {\olspecials \do \|}
  765 
  766 %\def \droite {\mathrel {\,\hbox {\large$\triangleright$}\,}}
  767 \def \droite {\mathrel{\tt =}}
  768 
  769 \makeatletter
  770 \def |{\baractive}
  771 \def \baractive {\futurelet\token \next@baractive}
  772 \def \eattoken #1{}
  773 \def \next@baractive{\let\do\eattoken
  774     \ifx \token>\droite\else \mid \let \do \relax \fi \do}
  775 
  776 
  777 \def \Def #1in{\mathprefix {let}#1\mathinfix{in}}
  778 \def \Let#1in{\mathprefix {let}#1\mathinfix{in}}
  779 \def \Reply#1to{\mathprefix {reply}#1\mathinfix{to}}
  780 \def \>{\droite}
  781 \def \And {\mathrel{\tt and}}
  782 \def \tuple #1{{\tt (}#1{\tt )}}
  783 \def \<#1> {\tuple {#1}}
  784 
  785 \let \bcup \cup
  786 \let \thd \th
  787 \def \fv {fv}
  788 \def \defines {::}
  789 \def \produces #1{\Ds\mathop{\Longrightarrow}^{#1}}
  790 \def \reduces {\longrightarrow}
  791 \let \red \reduces
  792 \let \redcham \mapsto
  793 
  794 \let \plus \tplus
  795 
  796 \makeatother
  797  
  798 
  799 \def \dd {{\cal D}}
  800 \def \pp {{\cal P}}
  801 
  802 \def \dv {dv}
  803 
  804 \def \redsoupe {\mathrel {\mathop {\red} \limits^s}}
  805 \let \redstruct \rightleftharpoons
  806 \let \redchaud \rightharpoonup
  807 \let \redfroid \leftharpoondown
  808 \let \cool \leftharpoondown
  809 \let \heat \rightharpoonup
  810 
  811 \def\redstep{\mathrel{\mathpalette\redstepaux{}}}
  812 \def\redstepaux#1{\vcenter{\hbox{\ooalign{\hfil
  813       \raise2pt \hbox{$\rightharpoonup$}\hfil\cr\hfil
  814       \lower2pt\hbox {$\leftharpoondown$}\hfil\crcr
  815       $\longrightarrow$}}}}
  816 
  817 
  818 \let \redsoupe \red
  819 \let \redx \red
  820 
  821 
  822 \def \Comment #1{}
  823 \let \agree \approx
  824 \quoteon
  825 
  826 \maketoken \int {int}
  827 
  828