X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmathql%2Fdoc%2Fmathql_macros.sty;h=8c8a851302800c5a060f211acc91fa9443b0706b;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=01b563f8d00de16d5a245b0a22fbee7a9cf0ffc5;hpb=468da7af4b52d01451073ff1cca5aa1949b9657f;p=helm.git

diff --git a/helm/mathql/doc/mathql_macros.sty b/helm/mathql/doc/mathql_macros.sty
index 01b563f8d..8c8a85130 100644
--- a/helm/mathql/doc/mathql_macros.sty
+++ b/helm/mathql/doc/mathql_macros.sty
@@ -1,9 +1,39 @@
-\usepackage{fguidi-defs} 
+\usepackage{amssymb}
 
-\newcommand{\secref}[1]{Section~\ref{#1}}
-\newcommand{\subsecref}[1]{Subsection~\ref{#1}}
-\newcommand{\figref}[1]{Figure~\ref{#1}}
+\newcommand\CURI[1]{\texttt{<#1>}}
+\newcommand\EM[1]{\noindent\hbox{\frenchspacing\em #1}}
+\newcommand\TT[1]{\noindent\hbox{\frenchspacing\tt #1}}
+\newcommand\RM[1]{\noindent\hbox{\frenchspacing\rm #1}}
+\newcommand\secref[1]{Section~\ref{#1}}
+\newcommand\subsecref[1]{Subsection~\ref{#1}}
+\newcommand\figref[1]{Figure~\ref{#1}}
+\newcommand\ie{{\frenchspacing i.e.}}
+\newcommand\oft{\mathrel :}
+\newcommand\lex{\exists}
+\newcommand\lall{\forall}
+\newcommand\sub{\subseteq}
+\newcommand\meet{\between}
+\newcommand\sand{\cap}
+\newcommand\sdor{\sqcup}
+\newcommand\sor{\cup}
+\newcommand\bigsor{\bigcup}
+\newcommand\app{\mathbin @}
+\newcommand\fa{\phi}
+\newcommand\fb{\psi}
+\newcommand\st{\mathrel |}
+\newcommand\p{{^\prime}}
+\newcommand\jolly{\mathbin\square}
+\newcommand\gdlap[2]{\vbox to 0pt {\vskip#2\hbox{#1}\vss}}
+\newcommand\setnames@[2]{&\gdlap{\kern2pt$#1$}{#2}} 
+\newcommand\imain[1]{{\offinterlineskip\lineskip=2pt\noindent
+  $\vcenter{\halign{\hss$##$\hss&##\hss\cr#1\crcr}}$}}
+\newcommand\iname[1]{\cr\hrulefill\setnames@{#1}{-1.0ex}\cr}
+\newcommand\irule[3]{\imain{#1 \iname{#2} #3}}
+\newcommand\spc{\hspace{1em}}
+\newcommand\icr{\cr}
+\newcommand\Nop{\noindent\hbox to 0pt{\vbox to 1ex{\vfil}\hfil}}
 
+\newcommand\BNF{\textsc{bnf}}
 \newcommand\CAML{\textsc{caml}}
 \newcommand\Galax{\textsc{galax}}
 \newcommand\HELM{\textsc{helm}}
@@ -19,45 +49,56 @@
 \newcommand\XML{\textsc{xml}}
 \newcommand\XQuery{\textsc{xquery}}
 
-\def\av{{\frenchspacing a.v.}}
-
-\def\D{\Delta}
-\def\G{\Gamma}
-\def\ES{\emptyset}
-\def\bigsum{\bigoplus}
-\def\daq{\mathrel{\Downarrow_q}}
-\def\dar{\mathrel{\Downarrow_r}}
-\def\distr{\mathbin\odot}
-\def\dprod{\mathbin\boxtimes} 
-\def\dsum{\mathbin\boxplus} 
-\def\g{(\G_s, \G_a, \G_g)}
-\def\get#1#2{#1(#2)}
-\def\prod{\mathbin\otimes} 
-\def\set#1#2#3{#1[#2 \gets #3]}
-\def\sum{\mathbin\oplus}
-
-\def\Boole{\TT{Boole}}
-\def\Listof{\TT{ListOf}}
-\def\Setof{\TT{SetOf}}
-\def\Str{\TT{String}}
-\def\Num{\TT{Num}}
-
-\def\All{\TT{All}}
-\def\Exp{\TT{Exp}}
-\def\F{\TT{F}}
-\def\For{\TT{For}}
-\def\Fst{\TT{Fst}}
-\def\Fsts{\TT{Fsts}}
-\def\Fun{\TT{Fun}}
-\def\Gen{\TT{Gen}}
-\def\Istrue{\TT{IsTrue}}
-\def\Match{\TT{Match}}
-\def\Name{\TT{Name}}
-\def\Pattern{\TT{Pattern}}
-\def\Property{\TT{Property}}
-\def\Snd{\TT{Snd}}
-\def\Src{\TT{Src}}
-\def\Unquote{\TT{Unq}}
-\def\T{\TT{T}}
-
-\def\GP#1{\TT{<#1>}}
+\newcommand\av{{\frenchspacing a.v.}}
+
+\newcommand\D{\Delta}
+\newcommand\G{\Gamma}
+\newcommand\ES{\emptyset}
+\newcommand\bigsum{\bigoplus}
+\newcommand\daq{\mathrel{\Downarrow_q}}
+\newcommand\dar{\mathrel{\Downarrow_r}}
+\newcommand\distr{\mathbin\odot}
+\newcommand\dprod{\mathbin\boxtimes} 
+\newcommand\dsum{\mathbin\boxplus} 
+\newcommand\g{(\G_s, \G_e, \G_g)}
+\newcommand\get[2]{#1(#2)}
+\newcommand\sdiff{\mathbin\ominus} 
+\newcommand\set[3]{#1[#2 \gets #3]}
+\newcommand\sprod{\mathbin\otimes} 
+\newcommand\ssum{\mathbin\oplus}
+
+\newcommand\Boole{\TT{Boole}}
+\newcommand\Listof{\TT{ListOf}}
+\newcommand\Setof{\TT{SetOf}}
+\newcommand\Str{\TT{Str}}
+\newcommand\Num{\TT{Num}}
+
+\newcommand\All{\TT{All}}
+\newcommand\Exp{\TT{Exp}}
+\newcommand\F{\TT{F}}
+\newcommand\For{\TT{For}}
+\newcommand\Fst{\TT{Fst}}
+\newcommand\Fsts{\TT{Fsts}}
+\newcommand\Fun{\TT{Fun}}
+\newcommand\Gen{\TT{Gen}}
+\newcommand\Head{\TT{Head}}
+\newcommand\Istrue{\TT{IsT}}
+\newcommand\Keep{\TT{Keep}}
+\newcommand\Match{\TT{Match}}
+\newcommand\Name{\TT{Name}}
+\newcommand\Pattern{\TT{Pattern}}
+\newcommand\Proj{\TT{Proj}}
+\newcommand\Property{\TT{Property}}
+\newcommand\Snd{\TT{Snd}}
+\newcommand\Src{\TT{Src}}
+\newcommand\Unquote{\TT{Unq}}
+\newcommand\T{\TT{T}}
+
+\newcommand\GP[1]{\TT{<#1>}}
+
+\newcommand\Set{\textsf{Set}}
+\newcommand\Prop{\textsf{Prop}}
+\newcommand\MainConclusion{\textsf{MainConclusion}}
+\newcommand\MainHypothesis{\textsf{MainHypothesis}}
+\newcommand\occurrence{\textsf{occurrence}}
+\newcommand\refObj{\textsf{refObj}}