X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=components%2Ftactics%2Fdoc%2Finfernce.sty;fp=components%2Ftactics%2Fdoc%2Finfernce.sty;h=fc4afeaaf400cd113d003691f3f0c734b3131af1;hp=0000000000000000000000000000000000000000;hb=f61af501fb4608cc4fb062a0864c774e677f0d76;hpb=58ae1809c352e71e7b5530dc41e2bfc834e1aef1 diff --git a/components/tactics/doc/infernce.sty b/components/tactics/doc/infernce.sty new file mode 100644 index 000000000..fc4afeaaf --- /dev/null +++ b/components/tactics/doc/infernce.sty @@ -0,0 +1,217 @@ +%% +%% 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'.