%
%  LaTeX Style file for Linear Logic
%  by Naoyuki Tamura (tamura@kobe-u.ac.jp)
%   2/15/1995
%   5/23/1996 modified
%
%  Linear Logic Connectives
%
\@ifundefined{multimap}{%
\newfont{\msamix}{msam9}
\newfont{\msamx}{msam10}
\newfont{\msamxi}{msam10 scaled \magstephalf}
\newfont{\msamxii}{msam10 scaled \magstep1}
\newfont{\msamxiv}{msam10 scaled \magstep2}
\@addfontinfo\@ixpt{\def\pmsam{\msamix}}
\@addfontinfo\@xpt{\def\pmsam{\msamx}}
\@addfontinfo\@xipt{\def\pmsam{\msamxi}}
\@addfontinfo\@xiipt{\def\pmsam{\msamxii}}
\@addfontinfo\@xivpt{\def\pmsam{\msamxiv}}
\def\msam{\protect\pmsam}
\def\maltese{\mbox{\msam\symbol{"7A}}}
\def\multimap{\mbox{\msam\symbol{"28}}}
%\input amssymbols.sty
}{}%
%
% Girard Notation
%
\def\girardnotation{%
  \def\drv{\;\vdash\;}%
  \def\lnot##1{{\def\arg{##1}\ifx\arg\empty()\else\arg\fi}{}^{\bot}}%
  \def\tprod{\otimes}%
  \def\tsum{\protect\raisebox{0.2ex}{$\wp$}}%
  \def\vartsum{\maltese}%
  \def\tunit{{\bf 1}}%
  \def\tzero{\bot}%
  \def\dprod{\mathop{\&}}%
  \def\dsum{\oplus}%
  \def\dunit{\top}%
  \def\dzero{{\bf 0}}%
  \def\limp{\mathop{\multimap}}%
  \def\lall{{\textstyle\bigwedge}}%
  \def\lexists{{\textstyle\bigvee}}%
}
%
% Troelstra Notation
%
\def\troelstranotation{%
  \def\drv{\;\Rightarrow\;}%
  \def\lnot##1{\mathop{\sim}##1}%
  \def\tprod{\star}%
  \def\tsum{+}%
  \def\tunit{{\bf 1}}%
  \def\tzero{{\bf 0}}%
  \def\dprod{\sqcap}%
  \def\dsum{\sqcup}%
  \def\dunit{\top}%
  \def\dzero{\bot}%
  \def\limp{\mathop{\multimap}}%
  \def\lall{\forall}%
  \def\lexists{\exists}%
}
%
% Default is Troelstra's notation
%
\troelstranotation
%
% Rule names
%
\def\LX{{\rm LX}}
\def\RX{{\rm RX}}
\def\Cut{{\rm Cut}}
\def\Ax{{\rm Ax}}
\def\Axiom{{\rm Axiom}}
\def\LR#1{{\rm L}#1}
\def\RR#1{{\rm R}#1}
\def\WR#1{{\rm W}#1}
\def\CR#1{{\rm C}#1}
\def\DR#1{{\rm D}#1}
%
% System Names
%
\def\CLL#1{\mbox{${\bf CLL}_{\rm #1}$}}
\def\ILZ#1{\mbox{${\bf ILZ}_{\rm #1}$}}
\def\ILL#1{\mbox{${\bf ILL}_{\rm #1}$}}