helm/ocaml/cic_notation/doc/shrthand.sty

   1 %%
   2 %% This is file `shrthand.sty',
   3 %% generated with the docstrip utility.
   4 %%
   5 %% The original source files were:
   6 %%
   7 %% semantic.dtx  (with options: `allOptions,shorthand')
   8 %%
   9 %% IMPORTANT NOTICE:
  10 %%
  11 %% For the copyright see the source file.
  12 %%
  13 %% Any modified versions of this file must be renamed
  14 %% with new filenames distinct from shrthand.sty.
  15 %%
  16 %% For distribution of the original source see the terms
  17 %% for copying and modification in the file semantic.dtx.
  18 %%
  19 %% This generated file may be distributed as long as the
  20 %% original source files, as listed above, are part of the
  21 %% same distribution. (The sources need not necessarily be
  22 %% in the same archive or directory.)
  23 %%
  24 %% semantic.dtx  (c)1995--2002 Peter M^^f8ller Neergaard and
  25 %%                             Arne John Glenstrup
  26 %%
  27 \expandafter\ifx\csname sem@nticsLoader\endcsname\relax
  28   \PackageError{semantic}{%
  29     This file should not be loaded directly}
  30     {%
  31       This file is an option of the semantic package.  It should not be
  32         loaded directly\MessageBreak
  33       but by using \protect\usepackage{semantic} in your document
  34         preamble.\MessageBreak
  35       No commands are defined.\MessageBreak
  36      Type <return> to proceed.
  37     }%
  38 \else
  39 \IfFileExists{DONOTUSEmathbbol.sty}{%
  40   \RequirePackage{mathbbol}
  41   \newcommand{\@bblb}{\textbb{[}}
  42   \newcommand{\@bbrb}{\textbb{]}}
  43   \newcommand{\@mbblb}{\mathopen{\mbox{\textbb{[}}}}
  44   \newcommand{\@mbbrb}{\mathclose{\mbox{\textbb{]}}}}
  45 }
  46 { \newcommand{\@bblb}{\textnormal{[\kern-.15em[}}
  47   \newcommand{\@bbrb}{\textnormal{]\kern-.15em]}}
  48   \newcommand{\@mbblb}{\mathopen{[\mkern-2.67mu[}}
  49   \newcommand{\@mbbrb}{\mathclose{]\mkern-2.67mu]}}
  50 }
  51 \mathlig{|-}{\vdash}
  52 \mathlig{|=}{\models}
  53 \mathlig{->}{\rightarrow}
  54 \mathlig{->*}{\mathrel{\rightarrow^*}}
  55 \mathlig{->+}{\mathrel{\rightarrow^+}}
  56 \mathlig{-->}{\longrightarrow}
  57 \mathlig{-->*}{\mathrel{\longrightarrow^*}}
  58 \mathlig{-->+}{\mathrel{\longrightarrow^+}}
  59 \mathlig{=>}{\Rightarrow}
  60 \mathlig{=>*}{\mathrel{\Rightarrow^*}}
  61 \mathlig{=>+}{\mathrel{\Rightarrow^+}}
  62 \mathlig{==>}{\Longrightarrow}
  63 \mathlig{==>*}{\mathrel{\Longrightarrow^*}}
  64 \mathlig{==>+}{\mathrel{\Longrightarrow^+}}
  65 \mathlig{<-}{\leftarrow}
  66 \mathlig{*<-}{\mathrel{{}^*\mkern-1mu\mathord\leftarrow}}
  67 \mathlig{+<-}{\mathrel{{}^+\mkern-1mu\mathord\leftarrow}}
  68 \mathlig{<--}{\longleftarrow}
  69 \mathlig{*<--}{\mathrel{{}^*\mkern-1mu\mathord{\longleftarrow}}}
  70 \mathlig{+<--}{\mathrel{{}^+\mkern-1mu\mathord{\longleftarrow}}}
  71 \mathlig{<=}{\Leftarrow}
  72 \mathlig{*<=}{\mathrel{{}^*\mkern-1mu\mathord\Leftarrow}}
  73 \mathlig{+<=}{\mathrel{{}^+\mkern-1mu\mathord\Leftarrow}}
  74 \mathlig{<==}{\Longleftarrow}
  75 \mathlig{*<==}{\mathrel{{}^*\mkern-1mu\mathord{\Longleftarrow}}}
  76 \mathlig{+<==}{\mathrel{{}^+\mkern-1mu\mathord{\Longleftarrow}}}
  77 \mathlig{<->}{\longleftrightarrow}
  78 \mathlig{<=>}{\Longleftrightarrow}
  79 \mathlig{|[}{\@mbblb}
  80 \mathlig{|]}{\@mbbrb}
  81 \newcommand{\evalsymbol}[1][]{\ensuremath{\mathcal{E}^{#1}}}
  82 \newcommand{\compsymbol}[1][]{\ensuremath{\mathcal{C}^{#1}}}
  83 \newcommand{\eval}[3][]%
  84   {\mbox{$\mathcal{E}^{#1}$\@bblb \texttt{#2}\@bbrb}%
  85    \ensuremath{\mathtt{#3}}}
  86 \newcommand{\comp}[3][]%
  87   {\mbox{$\mathcal{C}^{#1}$\@bblb \texttt{#2}\@bbrb}%
  88    \ensuremath{\mathtt{#3}}}
  89 \newcommand{\@exe}[3]{}
  90 \newcommand{\exe}[1]{\@ifnextchar[{\@exe{#1}}{\@exe{#1}[]}}
  91 \def\@exe#1[#2]#3{%
  92   \mbox{\@bblb\texttt{#1}\@bbrb$^\mathtt{#2}\mathtt{(#3)}$}}
  93 \fi
  94 \endinput
  95 %%
  96 %% End of file `shrthand.sty'.