pvs.sty

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -*- Mode: Tex -*- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% pvs.sty -- Style file for LaTeX-printing PVS theories and proofs
%% Author          : Sam Owre
%% Created On      : Fri Jan 22 11:26:51 1999
%% Last Modified By: Sam Owre
%% Last Modified On: Fri Jan 22 14:02:47 1999
%% Update Count    : 2
%% Status          : Alpha test
%% 
%% HISTORY
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% PVS
%% Copyright (C) 2006, SRI International.  All Rights Reserved.

%% This program is free software; you can redistribute it and/or
%% modify it under the terms of the GNU General Public License
%% as published by the Free Software Foundation; either version 2
%% of the License, or (at your option) any later version.

%% This program is distributed in the hope that it will be useful,
%% but WITHOUT ANY WARRANTY; without even the implied warranty of
%% MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
%% GNU General Public License for more details.

%% You should have received a copy of the GNU General Public License
%% along with this program; if not, write to the Free Software
%% Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA  02111-1307, USA.
%% --------------------------------------------------------------------
\RequirePackage{amsmath}
\def\pvsid#1{\textrm{#1}}
\def\pvskey#1{\textsc{\textrm{\lowercase{#1}}}}
\def\pvscmt#1{\textsf{#1}}
% [ ]
\def\pvsbracketl{\boldsymbol{\bigl[}}
\def\pvsbracketr{\boldsymbol{\bigr]}}
% [\# \#]
\def\pvsrectypel{\bigl[\#}
\def\pvsrectyper{\#\bigr]}
% ( )
\def\pvsparenl{\bigl(}
\def\pvsparenr{\bigr)}
% [| |]
\def\pvsbrackvbarl{\bigl[\hskip-3pt\bigl[}
\def\pvsbrackvbarr{\bigr]\hskip-3pt\bigr]}
% (| |)
\def\pvsparenvbarl{\bigl(\hskip-3pt\bigl[}
\def\pvsparenvbarr{\bigr]\hskip-3pt\bigr)}
% {| |}
\def\pvsbracevbarl{\bigl\{\hskip-3pt\bigl[}
\def\pvsbracevbarr{\bigr]\hskip-3pt\bigr\}}
% (: :)
\def\pvslistl{\bigl\langle}
\def\pvslistr{\bigr\rangle}
% (# #)
\def\pvsrecexprl{\bigl(\#}
\def\pvsrecexprr{\#\bigr)}

\def\pvsdeclspacing{0in}		% Set to \baselinestretch in article.

%\def\zbox#1{{\hbox to0pt{#1}}}
\def\zbox#1{{\hbox{#1}}}

\def\pvssuperscript#1#2{\mbox{\({#1}^{#2}\)}}
\def\pvssubscript#1#2{\mbox{\({#1}_{#2}\)}}

%\long\def\comment#1{} % multi-line comments