X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=components%2Ftactics%2Fdoc%2Fsemantic.sty;fp=components%2Ftactics%2Fdoc%2Fsemantic.sty;h=98257cab8288f0db0812c36e33a9f3d29e6fd413;hp=0000000000000000000000000000000000000000;hb=f61af501fb4608cc4fb062a0864c774e677f0d76;hpb=58ae1809c352e71e7b5530dc41e2bfc834e1aef1

diff --git a/components/tactics/doc/semantic.sty b/components/tactics/doc/semantic.sty
new file mode 100644
index 000000000..98257cab8
--- /dev/null
+++ b/components/tactics/doc/semantic.sty
@@ -0,0 +1,137 @@
+%%
+%% This is file `semantic.sty',
+%% generated with the docstrip utility.
+%%
+%% The original source files were:
+%%
+%% semantic.dtx  (with options: `general')
+%% 
+%% IMPORTANT NOTICE:
+%% 
+%% For the copyright see the source file.
+%% 
+%% Any modified versions of this file must be renamed
+%% with new filenames distinct from semantic.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
+%%
+\NeedsTeXFormat{LaTeX2e}
+\newcommand{\semanticVersion}{2.0(epsilon)}
+\newcommand{\semanticDate}{2003/10/28}
+\ProvidesPackage{semantic}
+  [\semanticDate\space v\semanticVersion\space]
+\typeout{Semantic Package v\semanticVersion\space [\semanticDate]}
+\typeout{CVSId: $Id$}
+\newcounter{@@conflict}
+\newcommand{\@semanticNotDefinable}{%
+  \typeout{Command \@backslashchar\reserved@a\space already defined}
+  \stepcounter{@@conflict}}
+\newcommand{\@oldNotDefinable}{}
+\let\@oldNotDefinable=\@notdefinable
+\let\@notdefinable=\@semanticNotDefinable
+\newcommand{\TestForConflict}{}
+\def\TestForConflict#1{\sem@test #1,,}
+\newcommand{\sem@test}{}
+\newcommand{\sem@tmp}{}
+\newcommand{\@@next}{}
+\def\sem@test#1,{%
+  \def\sem@tmp{#1}%
+  \ifx \sem@tmp\empty \let\@@next=\relax \else
+    \@ifdefinable{#1}{} \let\@@next=\sem@test \fi
+  \@@next}
+\TestForConflict{\@inputLigature,\@inputInference,\@inputTdiagram}
+\TestForConflict{\@inputReservedWords,\@inputShorthand}
+\TestForConflict{\@ddInput,\sem@nticsLoader,\lo@d}
+\def\@inputLigature{\input{ligature.sty}\message{ math mode ligatures,}%
+                     \let\@inputLigature\relax}
+\def\@inputInference{\input{infernce.sty}\message{ inference rules,}%
+                     \let\@inputInference\relax}
+\def\@inputTdiagram{\input{tdiagram.sty}\message{ T diagrams,}%
+                     \let\@inputTdiagram\relax}
+\def\@inputReservedWords{\input{reserved.sty}\message{ reserved words,}%
+                     \let\@inputReservedWords\relax}
+\def\@inputShorthand{\input{shrthand.sty}\message{ short hands,}%
+                     \let\@inputShorthand\relax}
+\toks1={}
+\newcommand{\@ddInput}[1]{%
+  \toks1=\expandafter{\the\toks1\noexpand#1}}
+\DeclareOption{ligature}{\@ddInput\@inputLigature}
+\DeclareOption{inference}{\@ddInput\@inputInference}
+\DeclareOption{tdiagram}{\@ddInput\@inputTdiagram}
+\DeclareOption{reserved}{\@ddInput\@inputReservedWords}
+\DeclareOption{shorthand}{\@ddInput\@inputLigature
+   \@ddInput\@inputShorthand}
+\ProcessOptions*
+\typeout{Loading features: }
+\def\sem@nticsLoader{}
+\edef\lo@d{\the\toks1}
+\ifx\lo@d\empty
+  \@inputLigature
+  \@inputInference
+  \@inputTdiagram
+  \@inputReservedWords
+  \@inputShorthand
+\else
+  \lo@d
+\fi
+\typeout{and general definitions.^^J}
+\let\@ddInput\relax
+\let\@inputInference\relax
+\let\@inputLigature\relax
+\let\@inputTdiagram\relax
+\let\@inputReservedWords\relax
+\let\@inputShorthand\relax
+\let\sem@nticsLoader\realx
+\let\lo@d\relax
+\TestForConflict{\@dropnext,\@ifnext,\@ifn,\@ifNextMacro,\@ifnMacro}
+\TestForConflict{\@@maxwidth,\@@pLineBox,\if@@Nested,\@@cBox}
+\TestForConflict{\if@@moreLines,\@@pBox}
+\def\@ifnext#1#2#3{%
+  \let\reserved@e=#1\def\reserved@a{#2}\def\reserved@b{#3}\futurelet%
+  \reserved@c\@ifn}
+\def\@ifn{%
+      \ifx \reserved@c \reserved@e\let\reserved@d\reserved@a\else%
+          \let\reserved@d\reserved@b\fi \reserved@d}
+\def\@ifNextMacro#1#2{%
+  \def\reserved@a{#1}\def\reserved@b{#2}%
+    \futurelet\reserved@c\@ifnMacro}
+\def\@ifnMacro{%
+  \ifcat\noexpand\reserved@c\noexpand\@ifnMacro
+    \let\reserved@d\reserved@a
+  \else \let\reserved@d\reserved@b\fi \reserved@d}
+\newcommand{\@dropnext}[2]{#1}
+\ifnum \value{@@conflict} > 0
+   \PackageError{Semantic}
+     {The \the@@conflict\space command(s) listed above have been
+      redefined.\MessageBreak
+      Please report this to turtle@bu.edu}
+     {Some of the commands defined in semantic was already defined %
+      and has\MessageBreak now be redefined. There is a risk that %
+      these commands will be used\MessageBreak by other packages %
+      leading to spurious errors.\MessageBreak
+      \space\space Type <return> and cross your fingers%
+}\fi
+\let\@notdefinable=\@oldNotDefinable
+\let\@semanticNotDefinable=\relax
+\let\@oldNotDefinable=\relax
+\let\TestForConflict=\relax
+\let\@endmark=\relax
+\let\sem@test=\relax
+\newdimen\@@maxwidth
+\newbox\@@pLineBox
+\newbox\@@cBox
+\newbox\@@pBox
+\newif\if@@moreLines
+\newif\if@@Nested \@@Nestedfalse
+\endinput
+%%
+%% End of file `semantic.sty'.