]> matita.cs.unibo.it Git - helm.git/blobdiff - components/tactics/doc/infernce.sty
branch for universe
[helm.git] / components / tactics / doc / infernce.sty
diff --git a/components/tactics/doc/infernce.sty b/components/tactics/doc/infernce.sty
new file mode 100644 (file)
index 0000000..fc4afea
--- /dev/null
@@ -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 <return> 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&#2\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'.