-
Notifications
You must be signed in to change notification settings - Fork 32
/
pvs.sty
66 lines (59 loc) · 2.25 KB
/
pvs.sty
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -*- 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