]> matita.cs.unibo.it Git - helm.git/blob - helm/ocaml/cic_notation/doc/shrthand.sty
tex macros, checked in disambiguation section from whelp paper
[helm.git] / 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'.