X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2Fdoc%2Finfernce.sty;fp=helm%2Focaml%2Ftactics%2Fdoc%2Finfernce.sty;h=0000000000000000000000000000000000000000;hb=55b82bd235d82ff7f0a40d980effe1efde1f5073;hp=fc4afeaaf400cd113d003691f3f0c734b3131af1;hpb=771ee8b9d122fa963881c876e86f90531bb7434f;p=helm.git diff --git a/helm/ocaml/tactics/doc/infernce.sty b/helm/ocaml/tactics/doc/infernce.sty deleted file mode 100644 index fc4afeaaf..000000000 --- a/helm/ocaml/tactics/doc/infernce.sty +++ /dev/null @@ -1,217 +0,0 @@ -%% -%% This is file `infernce.sty', -%% generated with the docstrip utility. -%% -%% The original source files were: -%% -%% semantic.dtx (with options: `allOptions,inference') -%% -%% IMPORTANT NOTICE: -%% -%% For the copyright see the source file. -%% -%% Any modified versions of this file must be renamed -%% with new filenames distinct from infernce.sty. -%% -%% For distribution of the original source see the terms -%% for copying and modification in the file semantic.dtx. -%% -%% This generated file may be distributed as long as the -%% original source files, as listed above, are part of the -%% same distribution. (The sources need not necessarily be -%% in the same archive or directory.) -%% -%% semantic.dtx (c)1995--2002 Peter M^^f8ller Neergaard and -%% Arne John Glenstrup -%% -\expandafter\ifx\csname sem@nticsLoader\endcsname\relax - \PackageError{semantic}{% - This file should not be loaded directly} - {% - This file is an option of the semantic package. It should not be - loaded directly\MessageBreak - but by using \protect\usepackage{semantic} in your document - preamble.\MessageBreak - No commands are defined.\MessageBreak - Type to proceed. - }% -\else -\TestForConflict{\@@tempa,\@@tempb,\@adjustPremises,\@inference} -\TestForConflict{\@inferenceBack,\@inferenceFront,\@inferenceOrPremis} -\TestForConflict{\@premises,\@processInference,\@processPremiseLine} -\TestForConflict{\@setLengths,\inference,\predicate,\predicatebegin} -\TestForConflict{\predicateend,\setnamespace,\setpremisesend} -\TestForConflict{\setpremisesspace,\@makeLength,\@@space} -\TestForConflict{\@@aLineBox,\if@@shortDivider} -\newtoks\@@tempa -\newtoks\@@tempb -\newcommand{\@makeLength}[4]{ - \@@tempa=\expandafter{\csname @@#2\endcsname} - \@@tempb=\expandafter{\csname @set#2\endcsname} % - \expandafter \newlength \the\@@tempa - \expandafter \newcommand \the\@@tempb {} - \expandafter \newcommand \csname set#1\endcsname[1]{} - \expandafter \xdef \csname set#1\endcsname##1% - {{\dimen0=##1}% - \noexpand\renewcommand{\the\@@tempb}{% - \noexpand\setlength{\the \@@tempa}{##1 #4}}% - }% - \csname set#1\endcsname{#3} - \@@tempa=\expandafter{\@setLengths} % - \edef\@setLengths{\the\@@tempa \the\@@tempb} % - } - -\newcommand{\@setLengths}{% - \setlength{\baselineskip}{1.166em}% - \setlength{\lineskip}{1pt}% - \setlength{\lineskiplimit}{1pt}} -\@makeLength{premisesspace}{pSpace}{1.5em}{plus 1fil} -\@makeLength{premisesend}{pEnd}{.75em}{plus 0.5fil} -\@makeLength{namespace}{nSpace}{.5em}{} -\newbox\@@aLineBox -\newif\if@@shortDivider -\newcommand{\@@space}{ } -\newcommand{\predicate}[1]{\predicatebegin #1\predicateend} -\newcommand{\predicatebegin}{$} -\newcommand{\predicateend}{$} -\def\inference{% - \@@shortDividerfalse - \expandafter\hbox\bgroup - \@ifstar{\@@shortDividertrue\@inferenceFront}% - \@inferenceFront -} -\def\@inferenceFront{% - \@ifnextchar[% - {\@inferenceFrontName}% - {\@inferenceMiddle}% -} -\def\@inferenceFrontName[#1]{% - \setbox3=\hbox{\footnotesize #1}% - \ifdim \wd3 > \z@ - \unhbox3% - \hskip\@@nSpace - \fi - \@inferenceMiddle -} -\long\def\@inferenceMiddle#1{% - \@setLengths% - \setbox\@@pBox= - \vbox{% - \@premises{#1}% - \unvbox\@@pBox - }% - \@inferenceBack -} -\long\def\@inferenceBack#1{% - \setbox\@@cBox=% - \hbox{\hskip\@@pEnd \predicate{\ignorespaces#1}\unskip\hskip\@@pEnd}% - \setbox1=\hbox{$ $}% - \setbox\@@pBox=\vtop{\unvbox\@@pBox - \vskip 4\fontdimen8\textfont3}% - \setbox\@@cBox=\vbox{\vskip 4\fontdimen8\textfont3% - \box\@@cBox}% - \if@@shortDivider - \ifdim\wd\@@pBox >\wd\@@cBox% - \dimen1=\wd\@@pBox% - \else% - \dimen1=\wd\@@cBox% - \fi% - \dimen0=\wd\@@cBox% - \hbox to \dimen1{% - \hss - $\frac{\hbox to \dimen0{\hss\box\@@pBox\hss}}% - {\box\@@cBox}$% - \hss - }% - \else - $\frac{\box\@@pBox}% - {\box\@@cBox}$% - \fi - \@ifnextchar[% - {\@inferenceBackName}%{}% - {\egroup} -} -\def\@inferenceBackName[#1]{% - \setbox3=\hbox{\footnotesize #1}% - \ifdim \wd3 > \z@ - \hskip\@@nSpace - \unhbox3% - \fi - \egroup -} -\newcommand{\@premises}[1]{% - \setbox\@@pBox=\vbox{}% - \dimen\@@maxwidth=\wd\@@cBox% - \@processPremises #1\\\end% - \@adjustPremises% -} -\newcommand{\@adjustPremises}{% - \setbox\@@pBox=\vbox{% - \@@moreLinestrue % - \loop % - \setbox\@@pBox=\vbox{% - \unvbox\@@pBox % - \global\setbox\@@aLineBox=\lastbox % - }% - \ifvoid\@@aLineBox % - \@@moreLinesfalse % - \else % - \hbox to \dimen\@@maxwidth{\unhbox\@@aLineBox}% - \fi % - \if@@moreLines\repeat% - }% -} -\def\@processPremises#1\\#2\end{% - \setbox\@@pLineBox=\hbox{}% - \@processPremiseLine #1&\end% - \setbox\@@pLineBox=\hbox{\unhbox\@@pLineBox \unskip}% - \ifdim \wd\@@pLineBox > \z@ % - \setbox\@@pLineBox=% - \hbox{\hskip\@@pEnd \unhbox\@@pLineBox \hskip\@@pEnd}% - \ifdim \wd\@@pLineBox > \dimen\@@maxwidth % - \dimen\@@maxwidth=\wd\@@pLineBox % - \fi % - \setbox\@@pBox=\vbox{\box\@@pLineBox\unvbox\@@pBox}% - \fi % - \def\sem@tmp{#2}% - \ifx \sem@tmp\empty \else % - \@ReturnAfterFi{% - \@processPremises #2\end % - }% - \fi% -} -\def\@processPremiseLine#1\end{% - \def\sem@tmp{#1}% - \ifx \sem@tmp\empty \else% - \ifx \sem@tmp\@@space \else% - \setbox\@@pLineBox=% - \hbox{\unhbox\@@pLineBox% - \@inferenceOrPremis #1\inference\end% - \hskip\@@pSpace}% - \fi% - \fi% - \def\sem@tmp{#2}% - \ifx \sem@tmp\empty \else% - \@ReturnAfterFi{% - \@processPremiseLine#2\end% - }% - \fi% -} -\def\@inferenceOrPremis#1\inference{% - \@ifnext \end - {\@dropnext{\predicate{\ignorespaces #1}\unskip}}% - {\@processInference #1\inference}% -} -\def\@processInference#1\inference\end{% - \ignorespaces #1% - \setbox3=\lastbox - \dimen3=\dp3 - \advance\dimen3 by -\fontdimen22\textfont2 - \advance\dimen3 by \fontdimen8\textfont3 - \expandafter\raise\dimen3\box3% -} -\long\def\@ReturnAfterFi#1\fi{\fi#1} -\fi -\endinput -%% -%% End of file `infernce.sty'.