doc-src/iman.sty

simplify "conjecture_shape" business, as a result of using FOF instead of CNF

% iman.sty : Isabelle Manual Page Layout
%
\typeout{Document Style iman. Released 17 February 1994}

\hyphenation{Isa-belle man-u-script man-u-scripts ap-pen-dix mut-u-al-ly}
\hyphenation{data-type data-types co-data-type co-data-types }

\let\ts=\thinspace

%usage: \iflabelundefined{LABEL}{if not defined}{if defined}
\newcommand{\iflabelundefined}[1]{\@ifundefined{r@#1}}


%%%INDEXING  use sedindex to process the index

\newcommand\seealso[2]{\emph{see also} #1}
\usepackage{makeidx}

%index, putting page numbers of definitions in boldface
\def\bold#1{\textbf{#1}}
\newcommand\fnote[1]{#1n}
\newcommand\indexbold[1]{\index{#1|bold}}

%for indexing constants, symbols, theorems, ...
\newcommand\cdx[1]{{\tt#1}\index{#1@{\tt#1} constant}}
\newcommand\sdx[1]{{\tt#1}\index{#1@{\tt#1} symbol}}

\newcommand\tdx[1]{{\tt#1}\index{#1@{\tt#1} theorem}}
\newcommand\tdxbold[1]{{\tt#1}\index{#1@{\tt#1} theorem|bold}}

\newcommand\mltydx[1]{{\tt#1}\index{#1@{\tt#1} ML type}}
\newcommand\xdx[1]{{\tt#1}\index{#1@{\tt#1} exception}}

\newcommand\ndx[1]{{\tt#1}\index{#1@{\tt#1} nonterminal}}
\newcommand\ndxbold[1]{{\tt#1}\index{#1@{\tt#1} nonterminal|bold}}

\newcommand\cldx[1]{{\tt#1}\index{#1@{\tt#1} class}}
\newcommand\tydx[1]{\textit{#1}\index{#1@{\textit{#1}} type}}
\newcommand\thydx[1]{{\tt#1}\index{#1@{\tt#1} theory}}

\newcommand\tooldx[1]{{\tt#1}\index{#1@{\tt#1} tool}}
\newcommand\settdx[1]{{\tt#1}\index{#1@{\tt#1} setting}}

%set argument in \tt font; at the same time, index using * prefix
\newcommand\rmindex[1]{{#1}\index{#1}\@}
\newcommand\ttindex[1]{{\tt#1}\index{*#1}\@}
\newcommand\ttindexbold[1]{{\tt#1}\index{*#1|bold}\@}

%set argument in \bf font and index in ROMAN font (for definitions in text!)
\newcommand\bfindex[1]{{\bf#1}\index{#1|bold}\@}


%%% underscores as ordinary characters, not for subscripting
%%  use @ or \sb for subscripting; use \at for @
%%  only works in \tt font
%%  must not make _ an active char; would make \ttindex fail!
\gdef\underscoreoff{\catcode`\@=8\catcode`\_=\other}
\gdef\underscoreon{\catcode`\_=8\makeatother}
\chardef\other=12
\chardef\at=`\@

% alternative underscore
\def\_{\leavevmode\kern.06em\vbox{\hrule height.2ex width.3em}\hskip0.1em}

%%% \dquotes permits usage of "..." for \hbox{...} -- also taken from under.sty
{\catcode`\"=\active
\gdef\dquotes{\catcode`\"=\active  \let"=\@mathText}%
\gdef\@mathText#1"{\hbox{\mathTextFont #1\/}}}
\def\mathTextFont{\frenchspacing\tt}
\def\dquotesoff{\catcode`\"=\other}

%%%% meta-logical connectives

\let\Forall=\bigwedge
\let\Imp=\Longrightarrow
\let\To=\Rightarrow
\newcommand{\PROP}{\mathop{\mathrm{PROP}}}
\newcommand{\Var}[1]{{?\!#1}}
\newcommand{\All}[1]{\Forall#1.}  %quantification

%%%% ``WARNING'' environment
\def\dbend{\vtop to 0pt{\vss\hbox{\Huge\bf!}\vss}}
\newenvironment{warn}{\medskip\medbreak\begingroup \clubpenalty=10000 
         \small %%WAS\baselineskip=0.9\baselineskip
         \noindent \hangindent\parindent \hangafter=-2 
         \hbox to0pt{\hskip-\hangindent\dbend\hfill}\ignorespaces}%
        {\par\endgroup\medbreak}