%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%% 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\lab{\mbox{\tt @}} \let\Lab=\lab %%\def\lab{\withmath{\tilde{\makebox[0.4em]\relax}}} %%\def\Lab{\withmath{\tilde{\makebox[0.4em]\relax}}} \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}}} % \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}} %% Program type-setting. %%\input{/tigger/saraswat/tex/cc-program-thesis-two-column.tex} % October 22, 1988, Vijay Saraswat (c) Xerox PARC % % Macros for typesetting cc (and FCP and GHC...) programs. % % Exported, top-level macros: \ax, \ag % % Exported environments: ccprogram, fccprogram, Frame % % Updated December 14, 1988. % Also, agent is introduced, with terminator .., since . is used for indexing. % Also ~ is used for label. % Also ++ gets \OrSep, + now gets plus. % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % The original code was from Eric Tribble. I have combined it % with the code I wrote modifying the LaTeX tabbing environment % so that each field is processed in math mode. % As it is now, this file should be used from now on for writing % new programs, rather than the old files. % To do: % Allow comment and Lists to span multiple lines. % Allow comment to be started off with --. % 10 November 1988 % Set up the \{ ... \} pairs. \{ starts off a + expression by % opening up a paren and then leaving enough space so that %successive uses of + produce a layout of the form: % ( Ag1 % + Ag2 % ... % + Ag3) % For example, try: %\begin{ccprog} %\ccag %p(X, State):: %\{ grab(X)\vop \then type\_A(State) %+ grab(X)\iop \then type\_B(State) %+ arbafhsiadhoashdis \tthen fasjofjsaod \}. %\end{ccprog} % There is some bogosity right now in how \} works: ideally % just a \-) should have worked, but it seems to reduce % first-tab-stop by 1 for the current line. I suspect this % might be interacting badly with \obeycr. For the time being % just use \} separately by itself on a line. %%%%%%%%%%%%%%%%%%%%% % Some space eating macros from latex.tex %\makeatletter %{\catcode`\^^M=13 \gdef\obeycrax{\catcode`\^^M=13 %\def^^M{\\ }\@gobblecr}% %Note that \obeycr is defined within latex.tex \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 } {% setup for the macro ax \axactivate \gdef\axpunct{% \axactivate \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{\;\char`\-\;} ##1\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`\[\begingroup\def|{\;\char`\|\;}}\def\[{\tt\char`\[} \def]{\char`\]\endgroup}\def\]{\char`\]} \def~{\Lab} \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 \eightpoint \else \ifx\sptabfont\sptabularx \vskip0pt %%\vskip2pt %%\hrule height .25pt %%\vskip.6pt \eightpoint\else \ifx\sptabfont\sptabbing \vskip0pt %%\vskip6pt %%\hrule height .25pt \eightpoint %%\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 \cp % 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}[theorem]{Proposition} \newtheorem{lemma}[theorem]{Lemma} \newtheorem{corollary}[theorem]{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}