%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% twocolumn
%%\input{/tigger/saraswat/tex/init-book-macros-two-column}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%This is an option to an article-type documentstyle, in which
%%the largest proper part of a document is a section. 
%% Changed all the counters so that they reset at every section,
%% rather than at every section. (21 January 1989)

\typeout{Document Style 'thesis-art-two-column'. (c) Vijay Saraswat November 1987.}
%% Macros used in the book. (c) Vijay Saraswat Xerox PARC
%% History
%% 24 November 1988. init-book-macros generated from
%% init-thesis-macros so that I could revert to using | for dcc
%% and & for dkc. 
%% (5 April 1989---no longer sure what the above comment means.
%% Presumably it means that in init-thesis-macros, | is used for
%% dcc etc.)
%% 22 October 1988  Added program macros from cc-program-thesis.tex
%% 2 August 1987. 
%% Make sure that all changes to this file are reflected also in 
%% thesis-art-macros.tex
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\def\const{{\tt const}}
\def\clu{{\bf CLU}}
\def\clpR{{\bf CLP($\Re$)}}
\def\fvar{{\bf fvar}}

\def\Hat{{\tt \char`\^}}
%\def\Hat{\mbox{\tt\^}}
%\def\Hat{\mbox{\tt\^{\makebox[0.4em]\relax}}}
\def\phia{\phi_{\ask}}\def\iotaa{\iota_{\ask}}
\def\phit{\phi_{\star}}\def\iotat{\iota_{\star}}
\def\prologiii{{\bf Prolog-III}}
\def\lvec{\overleftarrow}
\def\oexists{\overleftarrow{\exists}}
\let\outerex=\oexists
\def\dless{\sqsubseteq}
\def\shift{\gg}
\def\To{\mapsto}

\def\dthen{\;\hookrightarrow\;}
\def\ddc{\mathrel\hookrightarrow}
\def\qddc{``\withmath{\ddc}''}
\def\OrSeq{;;}
%%\def\Check{?}
\def\ai{AI}\def\sqb{{\tt \char`\[}}\def\sqbe{{\tt \char`\]}}
\def\makestat{\leadsto}
\def\av{\withmath{\star}}
\def\HANG{{\tt hang}}
\def\noteq{\mbox{$\;\not=\;$}}
\def\inst#1#2{#1\ \underline{{\tt inst}}\  #2}
\def\fix#1#2{#1\ \underline{{\tt fix}}\  #2}
\long\def\oneg{\underline{{\tt oneg}}\;}
\long\def\allg{\underline{{\tt allg}}\;}
\def\Nameoneg{\underline{{\tt oneg}}}
\def\Nameallg{\underline{{\tt allg}}}
\def\Nameinst{\underline{{\tt inst}}}
\def\Namefix{\underline{{\tt fix}}}
\def\Nameguard{\underline{{\tt guard}}}
\def\Namewfguard{\underline{{\tt wfguard}}}
\def\Namehpar{{\Uparrow}}
\def\Namesynth{\underline{{\tt synthesize}}}

\def\guard{\underline{{\tt guard}}\;}\def\wfguard{\underline{{\tt wfguard}}\;}
\def\hpar{\Uparrow}
\def\synth{\Namesynth\;}
\def\ballg{\underline{{\tt all}}\char`\(} %%\mbox{{\tt [}}}
\def\eallg{\char`\)}
%%\def\eallg{\mbox{{\tt ]}}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newsavebox{\OrSepBox}
%\savebox{\OrSepBox}{\mathrel\raisebox{0.6ex}{\framebox[0.4em]\relax}}
\def\OrSep{\;{\raisebox{0.6ex}{\framebox[0.4em]\relax}}\;}
%\usebox{\OrSepBox}\;}
\newsavebox{\ColSepBox} \savebox{\ColSepBox}{:\relax}
\def\ColSep{\usebox{\ColSepBox}\;}
\newsavebox{\AskBox} \savebox{\AskBox}{\raisebox{1.22ex}{\tenex \char'171}}
\newsavebox{\gAskBox} \savebox{\gAskBox}{\raisebox{1.22ex}{\tenex \char'177}}
\newsavebox{\InfrmBox} \savebox{\InfrmBox}{\raisebox{1.22ex}{\tenex \char'170}}
%%% The following inserted 15 Noveber 1988.
% Various Ask and Tell primitives.
%\def\ask{\withmath{\,\mbox{\leavevmode\raisebox{1.37ex}{\tenex \char'171}}\;}}
%\def\ask{\withmath{\,\leavevmode\raisebox{1.37ex}{\tenex \char'171}\;}}
\def\ask{\withmath{\,\usebox{\AskBox}\;}}
\def\iop{\usebox{\AskBox}}
\def\gask{\withmath{\,\usebox{\gAskBox}\;}}
\def\ep{\withmath{\;\ast}}
\def\ap{\withmath{\;\star}}
\def\infrm{\withmath{\,\usebox{\InfrmBox}\;}}
\let\vop=\infrm
\newcommand{\qvop}{``\vop''}

\def\STOP{{\tt stop}}
\def\PAR{\mathrel\Vert}

\def\qdc{``\dc''}
\def\dc{\withmath{\;\hookrightarrow\;}}
%% For don't-care prefixing (commitment):
\def\then{\withmath{\;\rightarrow\;}}

\def\dcc{\withmath{\rightarrow}}
\def\qdcc{``\dcc''}

%% For don't know prefixing (commitment):
\def\tthen{\withmath{\;\Rightarrow\;}}
\def\dkc{\withmath{\mathrel\Rightarrow}}
\def\qdkc{``\dkc''}
\def\qdk{\qdkc}
\def\qpdk{\qdkc}

%% For sequential don't know commitment
\def\sdk{\withmath{\mathrel{\Longrightarrow}}}
\def\sthen{\sdk}
\def\qsdk{``\sdk''}

\def\iot{\withmmode{\downarrow/2}}
\def\io{\withmmode{\downarrow/1}}
\def\vo{\withmmode{\uparrow}}
\newcommand{\qvo}{``\vo''}
\newcommand{\qio}{``\io''}
\newcommand{\qiot}{``\iot''}
\newcommand{\qiop}{``\iop''}
\newcommand{\qiopm}{``{\tt \iop  m}''}
\newcommand{\qiopT}{``{\tt \iop  T}''}
\newcommand{\ioa}{{\tt \iop  a}}
\newcommand{\iob}{{\tt \iop  b}}


% The following were superseded by the above definition.
%\def\ask{\iop}
%\def\gask{\withmath{\Downarrow}}
%\newcommand{\vop}{\withmath{\Hat}}
%For uparrow and downarrow! Taken from the TeXbook.
%\def\iop{\withmmode{\downarrow\!}}
%\newcommand{\Hat}{\withmath{\uparrow}}
%\def\iop{\withmath{{\tt \downarrow}}}
%\def\iop{\leavevmode\hbox{\tt\char'14}}
%\def\Hat{\leavevmode\hbox{\tt\char'13}}

\newcommand{\herbrandz}{\withmath{\ccfont herbrand_0}}
\newcommand{\ConsSep}{\withmath{\mathrel{\bowtie}}}
\newcommand{\isa}{\withmath{\mapsto}}
\newcommand{\LEQ}{\withmath{\leq\,\,}}
\newcommand{\SC}{{\bf SC}}
\newcommand{\mod}{\withmath{{\tt \;mod\;}}}
\newcommand{\GCD}{{\mbox{\em gcd}}}
\newcommand{\LSC}{\mbox{\bf LSC}}
\newcommand{\GSC}{\mbox{\bf GSC}}
\newcommand{\Con}{\mbox{\em Con}}
\newcommand{\cond}{\mbox{\bf cond}}
\newcommand{\Clause}{\mbox{\tt Clause}}

%\newcommand{\body}{$\Rightarrow$}
%\newcommand{\guard}{$\rightarrow$}

%\def\varn{{\tt\char"5E}} % this gets ^ in \tt font.

% Some macros used uniformly in the semantics sets of papers. 

%\newcommand{\etal}{\mbox{\it et al}}
\newcommand{\meet}{\withmath{\wedge}}
\newcommand{\join}{\withmath{\vee}}
\newcommand{\new}{new}
\newcommand{\CHECK}{\withmath{\surd}}
\newcommand{\Env}{\mbox{\bf Env}}
\newcommand{\known}{\mbox{\tt known}}
\newcommand{\ground}{\mbox{\tt ground}}
\newcommand{\nonvar}{\mbox{\tt nonvar}}

% Distinguish between alternation symbol and | by using different fonts. 

\def\alt{\withmmode{\;{\tt\char`\|}\;}}
\newcommand{\AND}{\;\&\;}
\newcommand{\CUT}{\mbox{$\:$`{\tt |}'$\:$}}
\newcommand{\Cut}{\mbox{$\:$`{\tt |}'$\:$}}
\newcommand{\var}{\mbox{\bf var}}
\def\const{\mbox{\bf const}}
\def\fvar{\mbox{\bf fvar}}
%\newcommand{\lub}{\mbox{\bf lub}}
%\newcommand{\cut}{cut}
\newcommand{\dom}{\mbox{\bf dom}}
%\newcommand{\cod}{\mbox{\bf cod}}
%\newcommand{\undefined}{\mbox{\it undefined}}
\newcommand{\compatible}{\mbox{\bf compatible}}
\newcommand{\bound}{\mbox{\bf bound}}
\newcommand{\unbound}{\mbox{\bf unbound}}
\newcommand{\defined}{\stackrel{\bf def}{=}}
\newcommand{\false}{\mbox{\tt false}}
\newcommand{\true}{\mbox{\tt true}}
\newcommand{\success}{\mbox{\tt true}}

\newcommand{\tderives}{\stackrel{\theta}{\longrightarrow}}
%\newcommand{\Vderives}{\stackrel{V}{\longrightarrow}}
%\newcommand{\VIDderives}{\stackrel{V,\Id}{\longrightarrow}}
%\newcommand{\tvderives}{\stackrel{V,\theta}{\derives}}
\newcommand{\starderives}{\derives^*}
\newcommand{\derives}{\longrightarrow}
\newcommand{\derivest}{\longmapsto}
\newcommand{\aderives}{\stackrel{\dkc}{\derives}}
\newcommand{\sderives}{\stackrel{\sigma}{\derives}}
\newcommand{\ssderives}{\stackrel{\sigma'}{\derives}}
\newcommand{\lderives}{\stackrel{\lambda}{\derives}}
\newcommand{\lambdaderives}{\stackrel{\lambda}{\longrightarrow}}
\newcommand{\lambdaderivest}{\stackrel{\lambda}{\longmapsto}}
\newcommand{\llderives}{\stackrel{\lambda'}{\derives}}
\newcommand{\lllderives}{\stackrel{\lambda''}{\derives}}
\newcommand{\acapprox}{\approx_1}
\newcommand{\aaapprox}{\approx_2}
\newcommand{\oaapprox}{\sim_2}
\newcommand{\oiapprox}{\sim_0}
\newcommand{\ocapprox}{\sim_1}
\newcommand{\rename}{\mbox{\bf rename}}
\newcommand{\asqsubseteq}{\sqsubseteq_{\dkc}}
\newcommand{\adoteq}{\doteq_{\dkc}}
\def\from#1\infer#2{{{\textstyle #1}\over{\textstyle #2}}}
\def\rname#1\from#2\infer#3{{{\textstyle #2}\over{\textstyle #3}}{\ \textstyle(#1)}}
\def\axname#1\axiom#2{{\textstyle #2}{\ \textstyle(#1)}}
% \sum\limits_{i\in I}

% \let\texsum=\sum
% \def\sum{\texsum\limits}

%Macros used in the transition system semantics for CP.

\def\longlongrightarrow{\relbar\joinrel\mathrel{\longrightarrow}}
%\newcommand{\k}{\backslash k}

\newenvironment{efmath}{\begin{equation}\begin{array}{|l|}\hline}{\\ \hline\end{array}\end{equation}}
%%The names of the semantically meaningful sets for logic programming
%% languages. 
\newcommand{\F}{\mbox{\it F}}
\newcommand{\D}{\mbox{\it D}}
\newcommand{\SS}{\mbox{\it SS}}
\newcommand{\FSS}{\mbox{\it FSS}}
\newcommand{\FFF}{\mbox{\it FFF}}
\newcommand{\FFFF}{\mbox{\it FFFF}}
\newcommand{\SSS}{\mbox{\it SSS}}
\newcommand{\FF}{\mbox{\it FF}}
\newcommand{\DD}{\mbox{\it DD}}
\newcommand{\II}{\mbox{\it II}}
%\newcommand{\lfp}{\mbox{\bf lfp}}
%\newcommand{\append}{\mbox{\it append}}
%\newcommand{\lab}{\mbox{\it Lab}}

% The control annotations used in CP languages. 
\newcommand{\Goal}{\mbox{\tt Goal}}
\newcommand{\Program}{\mbox{\tt Program}}
\newcommand{\comm}{\Downarrow}
\newcommand{\qqq}{\quad\quad\quad}
\newcommand{\qq}{\quad\quad}

% Introduced August 17, 1987. 
%\def\withmath#1{\ifmmode#1\else\ifinner#1 \else$#1$\fi\fi}
\def\withmmode#1{\relax\ifmmode#1\else{$#1$}\fi}
\def\withmath#1{\relax\ifmmode#1\else{$#1$}\fi}
\def\card#1{\withmmode{\mid \!#1\! \mid}}
\def\pair#1#2{\withmath{\langle #1,\; #2 \rangle}}
\def\tuple#1{\withmath{\langle #1 \rangle}}

\def\List#1{\withmath{{\tt [#1]}}}
\def\bb{\withmath{\backslash}}
\def\Nil{{\tt []}}
\def\Null{{\tt []}}

\def\Bag#1{\withmath{{\tt\{#1\}}}}
\def\bag#1{\withmath{{\tt\{#1\}}}}

%% Check whether these can be flushed. 
%% names of domains. 
\newcommand{\Subst}{\mbox{\it Subst}}
\newcommand{\Conf}{\mbox{\it Conf}}
\newcommand{\Var}{\mbox{\tt Var}}
\newcommand{\Term}{\mbox{\tt Term}}
\newcommand{\Atom}{\mbox{\tt Atom}}
\newcommand{\Sup}{\mbox{\bf sup}}

% The first set of commands provide some additional LaTeX environments. 
\newcommand{\Config}{\mbox{\bf Config}}
\newcommand{\ComplexConfig}{\mbox{\bf ComplexConfig}}

\newcommand{\fail}{\mbox{\tt fail}}
\newcommand{\done}{\mbox{\tt done}}
\newcommand{\lgets}{\leftarrow}
\newcommand{\repl}{\mbox{\bf replicate}}
\newcommand{\Id}{{\bf Id}}

\newcommand{\suspend}{\mbox{\it susp}}
\newcommand{\susp}{\mbox{\tt hang}}

\newcommand{\mgu}{\mbox{\bf mgu}}
\newcommand{\mgud}{$\mgu_{\downarrow}$}

\def\llb{\withmath{\lbrack\!\lbrack}}
\def\rrb{\withmath{\rbrack\!\rbrack}}

% Changed 7 August to allow use of built-in \ll
\def\LL#1{\withmath{\llb #1 \rrb}}
\def\entails{\withmath{\Rightarrow}}


\def\withmath#1{\relax\ifmmode#1\else{$ #1 $}\fi}
\def\plus{\withmath{\;\char`\+\;}}
%No carriage returns allowed within comment, at present.
\def\ccomment#1{%
    \begingroup%
	\settowidth{\hangindent}{/*\ }
	\noindent {\tt -}{\tt -} #1 %
    \endgroup}
\newlength{\globalparindent} \setlength{\globalparindent}{\parindent}

%%The following modifies LaTeX's tab environment such that each
%%field is processed in math mode, and tt font. Thus spacing is
%%as in math mode. Quite delicate. 
\makeatletter
\def\ccaxgtabmods{%
 \let\bmath=$%
 \def\@stopfield{\ifmmode\bmath\else\relax\fi\egroup}%
 \def\@startfield{\global\setbox\@curfield\hbox\bgroup%%
 \ifmmode\relax\else\bmath\fi\tt}%{ BRACE MATCH HACK
 \def\@contfield{\global\setbox\@curfield\hbox\bgroup%
 \ifmmode\relax\else\bmath\fi\tt\unhbox\@curfield}}
\makeatother

\def\axactivate{%
	\catcode`;=13\relax 
	\catcode`\:=13\relax 
%%	\catcode`\!=13\relax
	\catcode`\|=13\relax 
	\catcode`\[=13\relax 
	\catcode`\]=13\relax 
	\catcode`+=13\relax 
	\catcode`-=13\relax 
	\catcode`,=13\relax 
	\catcode`<=13\relax 
	\catcode`>=13\relax 
        \catcode`\~=13\relax
        \catcode`\==13\relax
        \catcode`\^=13\relax
	}
{% setup for the macro ax
    \axactivate
    \gdef\axpunct{%
	\axactivate\def\foobarbaz{o}
        \def^{\Hat}
        \def\lam{{\tt \char`134}}
	\def:##1{\ifx-##1\relax
	          \withmath\leftarrow% Only in Axioms.
		\else
                  \ifx:##1{\bf\;\char`\:\char`\:\;} %Only
							  %in
							  %Agents.
		  \else
		    \ifx=##1{\char`\:\char`\=}
                  \else {\;\char`\:\;} ##1 % Separate ask
						 % and tell--only
						 % in Axioms
		  \fi
                  \fi
		\fi}
	\def-##1{\if\noexpand>\noexpand##1\relax{\then}
                  \else\if\foobarbaz##1{\linarrow}\else{\;\char`\-\;} ##1\fi
                   \fi}
%Doesn't quite work for ==>. Use \sdk for it. 
	\def=##1{\if\noexpand>\noexpand##1\relax{\tthen}\else{\;\char`\=\;} ##1\fi}

%Allows || to appear as \PAR and | to appear as |.
	\def|##1{\ifx|##1\relax{\;\PAR\;}\else\ifx>##1{\;\hookrightarrow\;}
                 \else{\;{\tt\char`\|}\;} ##1 % Rest operator, in list.
                  \fi\fi}
                     %Carriage-returns within a list will elicit an error.
                     %We want to fix this later. 
        \def\|{\;{\tt \char`\|}\;}
	\def[{\char`\[}\def\[{\tt\char`\[\R}
	\def]{\char`\]}\def\]{\char`\]\L}
        \def~##1{\ifx>##1\relax{\;\leadsto\;}\else{\;{\tt\char`\~}\;}##1\fi}
        \def;{\;\char`\;\;}  % Redefined, 17 January 1989.
        \def,{\char`\,\;}
        \def<{\leavevmode\hbox{\tt\char`\<}}\def\lt{\char`\<}

	\def>##1{\if\noexpand>\noexpand##1{\gg}
                 \else{\leavevmode\hbox{\tt\char`\>}} ##1 % Rest operator, in list.
                  \fi}
        \def\gt{\char`\>}
%%	\def!{\ask}
	\def\:{\char`\: \>}
        \def\R{\=\+}\def\L{\-}
        \def\W{\hspace{\globalparindent}}
        \def\I{\W\R}
        \def+##1{\ifx+##1{\OrSep}\else{\plus}##1\fi}
        \def\{{\char`\{ \=\+ }\def\}{\char`\}\-}
	\def\({(\R}\def\){)\L} 
    }
} % end setup group
\makeatletter

\long\def\ccquery #1.{\pushtabs \leftarrow \=\+ #1. \-\\ \poptabs}
\long\def\ccag#1.{\pushtabs%
                  \hspace{\globalparindent}\=\+ \kill 
                  \hspace{-\globalparindent} #1 \- \\ \poptabs \@gobblecr}
\long\def\agent#1..{\pushtabs%
                   \hspace{\globalparindent}\=\+ \kill 
                   \hspace{-\globalparindent} #1. \- \\ \poptabs \@gobblecr}
\long\def\sagent#1..{\pushtabs%
                   \hspace{\globalparindent}\=\+ \kill 
                   \hspace{-\globalparindent} #1 \- \\ \poptabs \@gobblecr}
\long\def\ccax#1.{\pushtabs%
                  \hspace{\globalparindent}\=\+ \kill 
                  \hspace{-\globalparindent} #1. \- \\ \poptabs \@gobblecr}
%\long\def\ccax#1.{%
%	\hspace{\globalparindent}\= \+ \kill
%	\hspace{-\globalparindent}#1.\-}
%        %\poptabs\-}

\def\sptabular{tabular}
\def\sptabularx{tabular*}
\def\sptabbing{tabbing}
\def\begin#1{\@ifundefined{#1}{\def\@tempa{\@latexerr{Environment #1
  undefined}\@eha}}{\def\@currenvir{#1}\def\@tempa{\csname
  #1\endcsname}}\begingroup
\def\sptabfont{#1}
\ifmmode\else
\ifx\sptabfont\sptabular
\vskip0pt
%%\vskip2pt
%%\hrule height .25pt
%%\vskip.6pt
%VJ%\eightpoint
\tenpoint
\else
\ifx\sptabfont\sptabularx
\vskip0pt
%%\vskip2pt
%%\hrule height .25pt
%%\vskip.6pt
\tenpoint\else
\ifx\sptabfont\sptabbing
\vskip0pt
%%\vskip6pt
%%\hrule height .25pt
\tenpoint
%%\vskip-8pt
\fi\fi\fi\fi
\@tempa}

\def\end#1{\csname end#1\endcsname%
\def\sptabfont{#1}%
\ifmmode\else
\ifx\sptabfont\sptabular
%%\vskip.6pt
%%\hrule height .25pt
%%\vskip2pt
\vskip0pt
\else
\ifx\sptabfont\sptabularx
%%\vskip.6pt
%%\hrule height .25pt
%%\vskip2pt
\vskip0pt
\else
\ifx\sptabfont\sptabbing
%%\vskip1sp
%%\hrule height .25pt
%%\vskip2pt
\vskip0pt
\fi\fi\fi\fi\endgroup%
      \@checkend{#1}\if@ignore \global\@ignorefalse
                               \ignorespaces\fi}

\newenvironment{ccprogram}%
{%\ifvmode\nointerlineskip \makebox[.6\linewidth]\fi%
\begingroup\tt\axpunct\obeycr\ccaxgtabmods\begin{tabbing}}%
{\end{tabbing}\endgroup\ignorespaces\global\@ignoretrue}
\makeatother

%%\input{mit-cmfonts}
%%This extracted from a long message that Terry Ehling sent me. 
%% Tue Apr  4 18:35:57 1989
%% Vijay Saraswat
%% mit-cmfonts
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\font\thirtysixpoint=cmr10 at 36pt
\font\thirtysixbold=cmbx10 at 36pt
\font\tenpoint=cmr10
\font\tenbold=cmbx10
\font\tenit=cmti10
\font\boldfourteen=cmbx10 scaled \magstep2 %% used in Title
\font\twelverm=cmr10 scaled\magstep1
\font\eleven=cmr10 scaled \magstephalf   %% used in subtitle
\font\elevenbold=cmbx10 scaled \magstephalf   %% used in toc
\font\nine=cmr9
\font\boldeight=cmbx8

\font\eightrm=cmr8
\font\eightbf=cmbx8
\font\eightit=cmti8
\font\eighti=cmmi8
\font\eightsy=cmsy8
\font\eightsl=cmsl8
\font\eighttt=cmtt8

\font\sixrm=cmr6
\font\sixi=cmmi6
\font\sixsy=cmsy6

\font\fivei=cmmi5
\font\fivesy=cmsy5


\def\eightpoint{\def\rm{\fam0\eightrm}%
  \textfont0=\eightrm \scriptfont0=\sixrm
  \textfont1=\eighti \scriptfont1=\sixi \scriptscriptfont1=\fivei
  \textfont2=\eightsy \scriptfont2=\sixsy \scriptscriptfont2=\fivesy
  \def\it{\fam\itfam\eightit}%
  \textfont\itfam=\eightit
  \def\sl{\fam\slfam\eightsl}%
  \textfont\slfam=\eightsl
  \def\bf{\fam\bffam\eightbf}%
  \textfont\bffam=\eightbf
  \def\tt{\fam\ttfam\eighttt}%
  \textfont\ttfam=\eighttt
  \setbox\strutbox=\hbox{\vrule height8pt depth3pt width0pt}%
  \baselineskip=9pt\rm}





\newenvironment{Frame}{%
\begin{displaymath}%
\begin{array}{|l|}%
\hline%
\begin{minipage}[t]{\textwidth}}{%
\end{minipage}\\
\hline\end{array}
\end{displaymath}}


\newenvironment{fccprogram}{\begin{ccprogram}}{\end{ccprogram}}



%%\input{/tigger/saraswat/tex/program.tex}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%  File defines a number of LaTex macros for formatting cc programs.
%  Author: Vijay A. Saraswat
%  Confidential, All rights reserved. 
%  (c) Vijay A. Saraswat and Xerox PARC, 1987,1988
%  Macros defined:
%  Modification History:
%  July 10 1988: The program environment now does not automatically
%                do a \par before and after the program. 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\typeout{Document Style ``program'' by Vijay Saraswat, July 1987.}
% First input the file that modifies the tabbing environment so that all
% fields are output in tt font. 
%\input{/herbrand/saraswat/tex/program-tabbing.tex}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Section I. program and fprogram environments. 
% And now the program and axiom and fact commands for which all this has
% been done in the first place. 

%% program. Vanilla program. 
\newenvironment{program}{\axgtabmods\begin{tabbing}}{\end{tabbing}}
%\newenvironment{program}{\par\begin{tabbing}}{\end{tabbing}\par}

\makeatletter
\def\axgtabmods{%
 \def\bmath{\relax}
% \let\bmath=$%
 \def\@stopfield{\ifmmode\bmath\else\relax\fi\egroup}%
 \def\@startfield{\global\setbox\@curfield\hbox\bgroup%
 \ifmmode\relax\else\bmath\fi\tt}%{ BRACE MATCH HACK
 \def\@contfield{\global\setbox\@curfield\hbox\bgroup%
 \ifmmode\relax\else\bmath\fi\tt\unhbox\@curfield}}
\makeatother

\newenvironment{tprogram}{
\begin{displaymath}
\begin{array}{|l|}
\hline 
\begin{minipage}[t]{25in}
\begin{tabbing}}{
\end{tabbing}
\end{minipage}\\ 
\hline\end{array}
\end{displaymath}}


%% fprogram. Frames the program in a box. 
%%\newenvironment{fprogram}{
%%\par\bigskip
%%\begin{tabular}{|l|}
%%\hline 
%%\begin{minipage}[t]{25in}
%%\begin{tabbing}}{
%%\end{tabbing}
%%\end{minipage}\\ 
%%\hline\end{tabular}
%%\par\bigskip}
%%
%% Changed this since the MIT Press setting already gives hrules
%% before and after a tabular environment, automatically.
\newenvironment{fprogram}{\begin{program}}{\end{program}}

%% dprog. For listing 2 programs side by side, and enclosed within a frame. 
%%\newcommand{\dprog}[2]{\par\bigskip
%%\begin{tabular}{|ll|}\hline
%%\begin{minipage}[t]{25in}\begin{tabbing} #1 \end{tabbing} 
%%\end{minipage} & 
%%\begin{minipage}[t]{25in} \begin{tabbing} #2 \end{tabbing} 
%%\end{minipage} 
%%\\ \hline
%%\end{tabular}\bigskip}

\newcommand{\dprog}[2]{
\begin{tabular}{ll}
\begin{minipage}[t]{25in}\tabbing #1 \endtabbing 
\end{minipage} & 
\begin{minipage}[t]{25in} \tabbing #2 \endtabbing 
\end{minipage} \\
\end{tabular}}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% \ax sets things up such that default left margin spacing is provided for 
% the body goals, that are supposed to occur one per line. A tab stop has
% been set up at the marging which begins the argument block. In #2 (the 
% arguments in the head, one needs to set up tabstops and push and pop them
% only if one wants more than the default indentation. 
% See example in /usr/vas/thesis/thesis/clause-tex.tex
% Changed July 19, 1987 to clear the tabs after an axiom. 

\def\sclause #1:-#2.{$(\tt #1 \leftarrow #2.)$}
\def\clause #1:-#2,#3.{$(\tt #1 \leftarrow #2\ \dc\ #3.)$}
\def\iclause #1:-#2,#3.{$(\tt #1 \leftarrow #2\ \dc_i\ #3.)$}
\def\kclause #1:-#2,#3.{$(\tt #1 \leftarrow #2\ \dkc\ #3.)$}
\def\cclause #1:-#2,#3.{$(\tt #1 \leftarrow #2\ \dcc\ #3.)$}
\def\query #1.{\pushtabs\tt $\leftarrow$ \=\+ #1. \- \\ \poptabs}

% The usual case. Make sure that when it is numbered then the body is 
% indented in by the appropriate amount. 
\def\ax #1(#2):-#3.{
\pushtabs\tt #1\=(\=\+\+#2)$\leftarrow$\-\- \\ 
%#1\=(\=\+\+#2\\ \<)$\leftarrow$\-\- \\ 
\quad\quad\quad\=\+\kill 
#3.\-\\ 
\poptabs}
\def\goal #1(#2){\tt#1\=(\=\+\+#2)\-\-}
% Numbered clause. 
\def\axn #1.#2(#3):-#4.{
\pushtabs
({\em Rule $#1$}) \tt\quad #2\=(\=\+\+#3\\ \<)$\leftarrow$\-\- \\ 
({\em Rule $#1$})\quad\quad\quad\=\+\kill 
#4.\- \\ 
\poptabs }

% Whole clause on one line.
\def\caxs #1:-#2:#3.{\tt #1 $\leftarrow$ #2 : #3.\\ } 
\def\caxsh #1:-#2:#3.{
\tt #1 $\leftarrow$ \\
\pushtabs\quad\quad\quad\=\+\kill
 #2 :  #3.\-\\
 \poptabs}

\def\axs #1:-#2.{\tt #1 $\leftarrow$ #2.\\ } 
\def\axsn #1.#2:-#3.{({\em Rule $#1$})\tt #2 $\leftarrow$ #3.\\ } 

% Head is on one line, and the body appears indented on next line(s).
\def\axsh #1:-#2.{
\tt #1 $\leftarrow$\\ 
\pushtabs\quad\quad\quad\=\+\kill 
\tt #2.\-\\ \poptabs}
\def\axshn #1.#2:-#3.{
({\em Rule $#1$})\tt #2 $\leftarrow$\\ 
\pushtabs({\em Rule $#1$})\quad\quad\quad\=\+\kill #2.\-\\ 
\poptabs}
% \saxsh for a sequential clause. 
\def\saxsh #1:-#2.{
\tt #1 $\leftarrow$\\ 
\pushtabs\quad\quad\quad\=\+\kill 
#2;;\-\\ \poptabs}

\def\fact #1.{\tt #1.\\}
\def\factn #1.#2.{({\em Rule $#1$})\quad \tt #2.\\}
\def\bfact #1(#2).{
\pushtabs\tt #1\=(\=\+\+#2\\ \<).\\\-\- 
\poptabs}

%% For directives at the top level, such as modes etc. 
\def\dir :-#1.{\tt :- #1.\\}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Section III.
% Formatting for feature structures. 

\def\ptypes #1:#2(#3){\pushtabs\tt #1:#2$\langle$\=\+#3$\rangle$ \poptabs}
\def\ptype #1:#2(#3){
\pushtabs\tt #1:#2\=$\langle$\=\+\+#3 \\ \<$\rangle$\\
\poptabs}
\def\patype #1(#2){
\pushtabs\tt #1\=$\langle$\=\+\+#2 \<$\rangle$\\\-\- 
\poptabs}
\def\patypes #1(#2){\pushtabs\tt #1$\langle$\=\+ #2 $\rangle$\poptabs}

\def\ftypes #1:(#2){\tt #1:$\langle$#2 $\rangle$\\}
\def\ftype #1:(#2){\pushtabs\tt #1:\=$\langle$\=\+\+#2 \\ \<$\rangle$\\
\poptabs}
\def\fatype (#1){\pushtabs\tt $\langle$\=\+#1 $\rangle$\\ \poptabs}
\def\fatypes (#1){\tt $\langle$#1$\rangle$\\}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


%
% July 20, 1987. Maybe we may want to consider redoing this with \tabbing
% instead of with \tabular. 
%A step is used to write out a derivation step. A derivation step consists of
% three parts: the number of the clause, the current resolvent, with the
% selected goal underlined, and the substitution computed at the current step,
% in italics.  The current resolvent and substitution can both be quite large,
% hence we enclose them in  tabular env, thereby allowing the use of \\ to
% break lines at the place of use. We also use free-floating column separations
% rather than have rigid column separation between the current resolvent and
% the substitution.

%% The tabular hack.
%% Since I started using the MITPress mechanism for
%% putting programs between ruled lines, instead of putting them
%% in separate frames, other places where I used tabular became
%% broken. So here I use the original LaTeX
%% definition of tabular etc. directly, without going through
%% \begin{tabular} and \end{tabular}, which are trapped by the
%% MIT definitions. 
\def\step#1.#2.#3.{#1 & {\tt \tabular[t]{l} #2 \endtabular}
\hfill {\em \tabular[t]{l}$\tt #3 $\endtabular}\\}

\newenvironment{derivation}%
{\par\bigskip\begin{tabular}{cl}}%
{\end{tabular}\bigskip} 
\newcommand{\sel}[1]{$\tt \underline{\tt #1}$}

% For some weird reason this does not seem to be defined on the ERGO TeX 
% systems. Lifted from /../th/usr/misc/.tex/lib/macros/plain.tex

\def\_{\leavevmode \kern.06em \vbox{\hrule width.3em}}
\newcommand{\metadate}[1]{}

\def\offw{{\tt off}-wire}
\def\onw{{\tt on}-wire}


\def\aexists{\delta}
\def\aforall{\bigtriangledown}
\newenvironment{fmath}{$$\begin{array}{|l|} \hline}{ \\ \hline  \end{array}$$}
\newcommand{\elseq}{\withmath{{\bf \tilde{a}}}}
\newcommand{\varseq}{\withmath{X_0, \ldots, X_{k-1}}}
\newcommand{\termseq}{\withmath{t_0, \ldots, t_{k-1}}}
\newcommand{\ntermseq}{\withmath{t_0, \ldots, t_{n-1}}}
\def\rstrct{\withmath{\uparrow}}
\def\restrict{\withmath{\uparrow}}


%%%%%%%%%%%%%%%%%%%%% Typesetting Quotations %%%%%%%%%%%%%%%%%%%%%
%% From Page 205 of the TeX Book.                               %%
%% Placing quotations appropriately.                            %%
%% the following macro lays out the quotations flushed right, in%%
%% appropriate fonts.  I do not use the built in quotation      %%
%% environment  except in running text.                         %%
%%Attempting to get quotations at the end of the chapter right: %%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newenvironment{Startquotes}%
{\begingroup\bigskip  % begining of the quotes
 \def\eject{\endgroup\eject}
 \def\par{\ifhmode\/\endgraf\fi}\obeylines
 \small  \baselineskip=10pt \interlinepenalty=10000
 \leftskip=0pt plus 40pc minus \parindent \parfillskip=0pt
 \everypar{\sl}}%
{\endgroup\medskip}
\def\Realauthor#1(#2){\smallskip\noindent\rm--- #1\unskip\enspace(#2)}

% This is taken from the TeXbook, page 419(?)
% Use endquotes to place quotations at the end of a chapter.
\newenvironment{Endquotes}%
{\ifodd\thepage \else\vfill\eject\null\fi
\begingroup\bigskip\vfill  % begining of the quotes
\def\par{\ifhmode\/\endgraf\fi}\obeylines
\small \baselineskip=10pt \interlinepenalty=10000
\leftskip=0pt plus 40pc minus \parindent \parfillskip=0pt
 \everypar{\sl}}%
{\endgroup\eject}

%%%%%%%%%%%%% Modifying citations and references %%%%%%%%%%%%%%%%%%
%%The following modification will cause citations and references %%
%%that are not defined to appear in the output with the label    %%
%%that was used for them in the text, between a pair of ?...?.   %%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\makeatletter
\def\@citex[#1]#2{\if@filesw\immediate\write\@auxout{\string\citation{#2}}\fi
  \def\@citea{}\@cite{\@for\@citeb:=#2\do
    {\@citea\def\@citea{,\penalty\@m}\@ifundefined
       {b@\@citeb}{{\bf ??\@citeb??}\@warning
       {Citation `\@citeb' on page \thepage \space undefined}}%
\hbox{\csname b@\@citeb\endcsname}}}{#1}}


\def\ref#1{\@ifundefined{r@#1}{{\bf ??#1??}\@warning
   {Reference `#1' on page \thepage \space 
    undefined}}{\edef\@tempa{\@nameuse{r@#1}}\expandafter
    \@car\@tempa \@nil\null}}

\def\pageref#1{\@ifundefined{r@#1}{{\bf ??#1??}\@warning
   {Reference `#1' on page \thepage \space 
    undefined}}{\edef\@tempa{\@nameuse{r@#1}}\expandafter
    \@cdr\@tempa\@nil\null}}
\makeatother

%%%%%%%%%%%%%%%%%%%%%%% Special Treatment for Proof %%%%%%%%%%%%%%%%
%% The following is a special treatment of Proof. The idea is     %%
%% that a Proof environment should only follow a Theorem          %%
%% environment or something aliased to one, for example a         %%
%% Proposition. So proof will not bump up the counter, but will   %%
%% read the current number of this counter. At this point we are  %%
%% assuming that a command called  \thetheorem has been           %%
%% defined.                                                       %%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Old version:
%%\newenvironment{proof}{\myproof}{\endmyproof}
\makeatletter
\def\theproof{\thetheorem}
\def\proof{\@ifnextchar[{\@ytxm{theorem}{Proof}}{\@xtxm{theorem}{Proof}}}
\def\endproof{\@endtenv}
\makeatother
%% This, because in other places I use \BEGproof etc.
\let\BEGproof=\proof \let\begproof=\proof \let\ENDproof=\endproof


%%\input{/tigger/saraswat/tex/languages}
%%\input{/tigger/saraswat/tex/new-initlanguages.tex}
% Nomenclature revised 31 March 1988
% Adopted cc as the prefix.
% Also the basic language is flat, The language with 
% the user-defined constraints is ucc.
% Hence 
% Control construct     Indicator   TexPrefix
%    guards               u             u
% CLP and other languages. (nomenclature revised 25 October 1987.)
% Systematic Nomenclature for members in the \cp\ family.
% The name of the TeX macro is \<prefix>cp<postfix>
% where prefix is one of {d, e,f} and postfix is a string
% of TexIndicators.
% control construct indicators:
%  Control Constuct      Indicator   TexIndicator    
% don't know commit        &          a
% don't care commit        |          d
% wait                     !          i
% freeze                   f          f
% otherwise                o          o
% And-sequentiality        ;          s
% Or-sequentiality         ;;         ss
% blocks                  [...]       b
%  Prefixes:
%  Control Constuct      Indicator   Tex Prefix
% flat language            f          f  
% determinate language     d          d  
% extended language        e          e  
%            Some shorthands
%  Language       Tex Indicator
% cp[!,|,&,;,o]      l
%% precedence ordering {f, d} < {c} < {a} < {s} < {ss, o} 
%% In the Tex Name, the indicators appear in the order 
%% in which the indicators appear in the name of the language. 

\newcommand{\ccfont}{\sf}
\newcommand{\ccba}{{\ccfont cc/ba}}
\newcommand{\cctwo}{{\ccfont 2-cc}}
\newcommand{\cca}{{\ccfont cc(\dkc)}}
\newcommand{\ccd}{{\ccfont cc(\dcc)}}
\newcommand{\ccie}{{\ccfont cc(\iop,\ep)}}
\newcommand{\cciapd}{{\ccfont cc(\iop,\ap,\dcc)}}
\newcommand{\cciapda}{{\ccfont cc(\iop,\ap,\dcc,\dkc)}}
\newcommand{\cciapevda}{{\ccfont cc(\iop,\ap, \ev,\dcc,\dkc)}}
\newcommand{\ccievda}{{\ccfont cc(\iop,\ev,\dcc,\dkc)}}
\newcommand{\ccievd}{{\ccfont cc(\iop,\ev,\dcc)}}

\newcommand{\ccide}{{\ccfont cc(\iop,\ep,\dcc)}}
\newcommand{\cci}{{\ccfont cc(\iop)}}
\newcommand{\uccda}{{\ccfont cc(\dcc,g,\dkc)}}
\newcommand{\ccda}{{\ccfont cc(\dcc,\dkc)}}
\newcommand{\ccid}{{\ccfont cc(\iop,\dcc)}} 
\newcommand{\ccia}{{\ccfont cc(\iop,\dkc)}}
\newcommand{\ccida}{{\ccfont cc(\iop,\dcc,\dkc)}}
\newcommand{\ccdas}{{\ccfont cc(\dcc;\dkc)}}
\newcommand{\ccids}{{\ccfont cc(\iop;\dcc)}}
\newcommand{\ccidasss}{{\ccfont cc(\iop;\dcc;;\dkc)}}
\newcommand{\ccfdo}{{\ccfont cc(f,\dcc,o)}}
\newcommand{\ccfda}{{\ccfont cc(f,\dcc,\dkc)}}
\newcommand{\ccfdao}{{\ccfont cc(f,\dcc,\dkc,o)}}
\newcommand{\wccfdao}{{\ccfont wcc(f,\dcc,\dkc,o)}}
\newcommand{\ccfdaso}{{\ccfont cc(f,\dcc,\dkc; o)}}
\newcommand{\ccdaso}{{\ccfont cc(\dcc,\dkc; o)}}
\newcommand{\ccdao}{{\ccfont cc(\dcc,\dkc,o)}}
\newcommand{\cc}{{\ccfont cc}}
\newcommand{\bfcc}{{\ccfont bcc}}
\newcommand{\gcc}{{\ccfont gcc}}
\newcommand{\ccfull}{{\ccfont cc(\iop,\dcc,\dkc)}}
\def\ccidv{{\ccfont cc(\iop,\dcc,\vop)}}
\def\cciapd{{\ccfont cc(\iop,\withmath{\star},\dcc)}}
\def\cciepd{{\ccfont cc(\iop,\withmath{\ast},\dcc)}}

\newcommand{\ucc}{{\ccfont cc}}
\newcommand{\ucca}{{\ccfont cc(g,\dkc)}}
\newcommand{\uccd}{{\ccfont cc(g,\dcc)}}
\newcommand{\uccdao}{{\ccfont cc(g,\dcc,\dkc,o)}}
\newcommand{\uccia}{{\ccfont cc(\iop,g,\dkc)}}
\newcommand{\uccid}{{\ccfont cc(\iop,g,\dcc)}}
\newcommand{\uccida}{{\ccfont cc(\iop,g,\dcc,\dkc)}}
\newcommand{\uccidas}{{\ccfont cc(\iop,g,\dcc;\dkc)}}
\newcommand{\uccfda}{{\ccfont cc(f, g,\dcc,\dkc)}}
\newcommand{\uccfdao}{{\ccfont cc(f, g, \dcc,\dkc,o)}}
\newcommand{\uccfdaso}{{\ccfont cc(f, g, \dcc,\dkc; o)}}
\newcommand{\uccdaso}{{\ccfont cc(\dcc, g, \dkc; o)}}

\newcommand{\hbuccida}{{\ccfont cc(\iop, g, \dcc,\dkc)/hb}}
\newcommand{\hbuccid}{{\ccfont cc(\iop, g, \dcc)/hb}}
\newcommand{\hbccid}{{\ccfont cc(\iop, g,   \dcc)/hb}}
\newcommand{\hbcc}{{\ccfont cc/hb}}

\newcommand{\clpr}{{CLP($\cal R$)}}
\def\clu{{\bf CLU}}

% The following macros will be phased out shortly. (31 March 1988)
\newcommand{\herbrand}{{\ccfont Herbrand}}
\def\Herbrand{{\ccfont Herbrand}}
\newcommand{\datacc}{{\ccfont data cc}}
\newcommand{\cpba}{{\ccfont cc/ba}}
\newcommand{\cptwo}{{\ccfont 2-cc}}
\newcommand{\cpa}{{\ccfont cc(\dkc)}}
\newcommand{\cpd}{{\ccfont cc(\dcc)}}
\newcommand{\cpda}{{\ccfont cc(\dcc,\dkc)}}
\newcommand{\cpid}{{\ccfont cc(\iop,\dcc)}}
\newcommand{\cpia}{{\ccfont cc(\iop,\dkc)}}
\newcommand{\cpida}{{\ccfont cc(\iop,\dcc,\dkc)}}
\newcommand{\cpidas}{{\ccfont cc(\iop,\dcc;\dkc)}}
\newcommand{\cpdas}{{\ccfont cc(\dcc;\dkc)}}
\newcommand{\cpidasss}{{\ccfont cc(\iop;\dcc;;\dkc)}}
\newcommand{\cpfdo}{{\ccfont cc(f,\dcc,o)}}
\newcommand{\cpfda}{{\ccfont cc(f,\dcc,\dkc)}}
\newcommand{\cpfdao}{{\ccfont cc(f,\dcc,\dkc,o)}}
\newcommand{\wcpfdao}{{\ccfont wcc(f,\dcc,\dkc,o)}}
\newcommand{\cpfdaso}{{\ccfont cc(f,\dcc,\dkc; o)}}
\newcommand{\cpdaso}{{\ccfont cc(\dcc,\dkc; o)}}
\newcommand{\cpdao}{{\ccfont cc(\dcc,\dkc,o)}}
\newcommand{\cp}{{\ccfont cc}}

% Other logic programming languages. 
\newcommand{\parlog}{{Parlog}}
\newcommand{\PrologIII}{{Prolog-III}}
\newcommand{\icprolog}{{IC-Prolog}}
\newcommand{\oc}{{\"{O}c}}
\newcommand{\CP}{{Concurrent Prolog}}
\newcommand{\Cp}{{Concurrent Prolog}}
\newcommand{\FCP}{{Flat Concurrent Prolog}}
\newcommand{\fghc}{{FGHC}}
\newcommand{\ghc}{{GHC}}
\newcommand{\prolog}{{Prolog}}
\newcommand{\Prolog}{{Prolog}}
\newcommand{\alps}{{ALPS}}
\newcommand{\FCPA}{{FCP(@)}}

\newcommand{\Juno}{{Juno}}
\newcommand{\CLPR}{{CLP(\withmath{\Re})}}
\newcommand{\Linda}{{Linda}}
\newcommand{\mlisp}{{MultiLisp}}
\newcommand{\Lisp}{{Lisp}}
\newcommand{\icon}{{Icon}}
%\newcommand{\CommonLisp}{{\bf CommonLisp}}
\newcommand{\Lucid}{{Lucid}}
\newcommand{\lucid}{{Lucid}}
%\newcommand{\Props}{{PROPS}}
%\newcommand{\kcinference}{{\bf KC-Inference}}
\newcommand{\C}{{C}}
\newcommand{\ops}{{Ops-5}}
%\newcommand{\Ops}{{Ops-5}}
\newcommand{\Pascal}{{ Pascal}}
\newcommand{\Actors}{{Actors}}
\newcommand{\ccs}{{CCS}}
\newcommand{\sccs}{{SCCS}}
\newcommand{\csp}{{CSP}}
\newcommand{\cspio}{{CSP/io}}

\def\hbid{{\ccfont \herbrand(\iop,\dcc)}}
\def\hbida{{\ccfont \herbrand(\iop,\dcc,\dkc)}}
\def\CPid{{{\bf CP}(\iop,{\tt |})}}
\def\CPida{{{\bf CP}(\iop,{\tt |}, {\tt \&})}}
\newsavebox{\wfhbidaBox}
\savebox{\wfhbidaBox}{{\ccfont \herbrand(\iop,w,\dcc,\dkc)}}
\def\wfhbida{\usebox{\wfhbidaBox}}
\def\wfccida{{\ccfont cc(\iop, w,\dcc,\dkc)}}







%\newtheorem{theorem}{Theorem}[section]
%\newtheorem{proposition}{Proposition}[section]
%\newtheorem{lemma}{Lemma}[section]
%\newtheorem{corollary}[lemma]{Corollary}

%\newtheorem{conjecture}{Conjecture}[section]
%\newtheorem{Fact}{Fact}[section]
%\newtheorem{Rule}{Rule}[section]

%%Check out comment in thesis-macros.tex.

%%\input{/tigger/saraswat/tex/thm-like}
%% A modified newtheorem command. Vijay Saraswat (c) Xerox PARC
%% 22 October 1988
%% Modified from Leslie Lamort's \LaTeX\ system. 
%% Command exported: \newtenv{#1}[#2]{#3}. 
%% Arguments are just like the arguments in \newtheorem,
%% except that the body of the text is not typeset in italics
%% and at the end of the text, we typset a framebox ---an end of 
%% environment marker---flushright at the end of the current
%% line. 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\makeatletter
\newsavebox{\eStop}
\savebox{\eStop}{\raisebox{0.6ex}{\framebox[0.5em]\relax}}

\def\newtenv#1{\@ifnextchar[{\@otxm{#1}}{\@ntxm{#1}}}

\def\@ntxm#1#2{\@ifnextchar[{\@xntxm{#1}{#2}}{\@yntxm{#1}{#2}}}

\def\@xntxm#1#2[#3]{\expandafter\@ifdefinable\csname #1\endcsname
{\@definecounter{#1}\@addtoreset{#1}{#3}%
\expandafter\xdef\csname the#1\endcsname{\expandafter\noexpand
  \csname the#3\endcsname \@thmcountersep \@thmcounter{#1}}%
\global\@namedef{#1}{\@txm{#1}{#2}}\global\@namedef{end#1}{\@endtenv}}}

\def\@yntxm#1#2{\expandafter\@ifdefinable\csname #1\endcsname
{\@definecounter{#1}%
\expandafter\xdef\csname the#1\endcsname{\@thmcounter{#1}}%
\global\@namedef{#1}{\@txm{#1}{#2}}\global\@namedef{end#1}{\@endtenv}}}

\def\@otxm#1[#2]#3{\expandafter\@ifdefinable\csname #1\endcsname
  {\global\@namedef{the#1}{\@nameuse{the#2}}%
\global\@namedef{#1}{\@txm{#2}{#3}}%
\global\@namedef{end#1}{\@endtenv}}}

\def\@txm#1#2{\refstepcounter
    {#1}\@ifnextchar[{\@ytxm{#1}{#2}}{\@xtxm{#1}{#2}}}

\def\@xtxm#1#2{\@begintenv{#2}{\csname the#1\endcsname}\ignorespaces}
\def\@ytxm#1#2[#3]{\@opargbegintenv{#2}{\csname
       the#1\endcsname}{#3}\ignorespaces}

%DEFAULT VALUES
\def\@begintenv#1#2{\trivlist \item[\hskip \labelsep{\bf #1\ #2}]}
\def\@opargbegintenv#1#2#3{\trivlist
      \item[\hskip \labelsep{\bf #1\ #2\ (#3)}]}
\def\@endtenv{\hfill\usebox{\eStop}\endtrivlist}
\makeatother
\newtenv{assumption}{Assumption}[section]
\newtenv{convention}{Convention}[section]
%\newtenv{example}{Example}[section]
\newtenv{comment}{Comment}[section]
\newtenv{digression}{Digression}[section]

%\newtenv{defin}{Definition}[section]
%\newtenv{definition}[defin]{Definition}

%\newtenv{note}{Note}[section]
\newtenv{reviewer-note}[note]{Note for the reviewer}
\newtenv{meta-note}[note]{MetaNote}
\newtenv{hist-note}[note]{Historical Note}
\newtenv{restriction}[note]{Restriction}

