The operational semantics of the core language is ready

[helm.git] / helm / mathql / doc / fguidi-defs.sty

diff --git a/helm/mathql/doc/fguidi-defs.sty b/helm/mathql/doc/fguidi-defs.sty
new file mode 100644 (file)
index 0000000..df71b44
--- /dev/null
+++ b/helm/mathql/doc/fguidi-defs.sty
@@ -0,0 +1,121 @@
+%\DeclareSymbolFont{stmary}{U}{stmary}{m}{n}
+%\DeclareFontFamily{U}{stmary}{}%
+%\DeclareFontShape{U}{stmary}{m}{n}{<-6>stmary5<6-8>stmary7<8->stmary10}{}%
+%\DeclareMathSymbol{\odb}{\mathopen}{stmary}{"4A}
+%\DeclareMathSymbol{\cdb}{\mathclose}{stmary}{"4B}
+
+\usepackage{amssymb}
+\usepackage{stmaryrd}
+
+% LOGIC  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
+
+% utilities
+
+\def\cv{\,]}
+\def\ov{[\,}
+\def\spc{\hspace{1em}} % 0.25em per la tesi
+\def\nop{{}}
+\def\Nop{\noindent\hbox to 0pt{\vbox to 1ex{\vfil}\hfil}}
+\def\gdlap#1#2{\vbox to 0pt {\vskip#2\hbox{#1}\vss}}
+\def\?#1{\mathord{#1}}
+
+% inference trees
+
+\def\imain#1{{\offinterlineskip\lineskip=2pt\noindent
+  \hbox{$\vcenter{\halign{\hss$##$\hss&##\hss\cr#1\crcr}}$}}}
+\def\itree#1{{\offinterlineskip\lineskip=2pt\noindent
+  \hbox{$\vbox{\halign{\hss$##$\hss&##\hss\cr#1\crcr}}$}}}
+
+\def\setnames@#1#2{&\gdlap{\kern2pt$#1$}{#2}} 
+\def\iname#1 {\cr\hrulefill\setnames@{#1}{-1.0ex}\cr}
+\def\inames#1 {\cr\hrulefill\cr\hrulefill\setnames@{#1}{-1.2ex}\cr}
+\def\ivrule{\cr\vrule height 3ex \cr}
+\def\discharge#1#2 {\iname{#1\,#2} }
+\def\assume#1#2{\ov #1\cv\rlap{$^{#2}$}}
+
+% single rules
+
+\def\irule#1#2#3{\imain{#1 \iname{#2} #3 }}   % "single step"
+\def\irules#1#2#3{\imain{#1 \inames{#2} #3 }} % "multistep"
+
+\def\drule#1#2#3{\itree{#1 \iname{#2} #3 }}   % "single step"
+\def\drules#1#2#3{\itree{#1 \inames{#2} #3 }} % "multistep"
+
+\def\cirule#1#2#3{$\vcenter{\irule{#1}{#2}{#3}}$}   % "single step"
+\def\cirules#1#2#3{$\vcenter{\irules{#1}{#2}{#3}}$} % "multistep"
+
+% MATHEMATICS  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\def\a{\phi}
+\def\b{\psi}
+\def\c{\xi}
+\def\d{\eta}
+\def\A{\Phi}
+\def\B{\Psi}
+\def\C{\Xi}
+\def\jolly{\mathbin\square}
+\def\lall{\forall}
+\def\lex{\exists}
+\def\lbot{{\bot}}
+\def\lexcl{\mathrel\leftarrow}
+\def\limp{\mathrel\rightarrow}
+\def\liff{\mathrel\leftrightarrow}
+\def\lone{1}
+\def\lplus{\mathrel\oplus}
+\def\ltimes{\mathrel\otimes}
+\def\ltop{{\top}}
+\def\lzero{0}
+\def\lpar{\mathrel\bindnasrepma}
+\def\lamp{\mathrel\binampersand}
+
+\def\meet{\between}
+\def\bigsor{\bigcup}
+\def\bigsand{\bigcap}
+\def\sand{\cap}
+\def\sdor{\sqcup}
+\def\sor{\cup}
+\def\simp{\Rightarrow}
+\def\snot{-}
+\def\sub{\subseteq}
+\def\sup{\supseteq}
+\def\sbot{\emptyset}
+\def\stop{\ltop}
+
+\def\after{\mathbin\circ}
+\def\app{\mathbin @}
+\def\e{\mathrel\epsilon}
+\def\oft{\mathrel :}
+\def\p{{^\prime}}
+\def\st{\mathrel |}
+\def\subset#1{\{#1\}}
+\def\yld{\mathrel\vdash}
+\def\Frm{\textsf{Frm}}
+\def\Trm{\textsf{Trm}}
+\def\LB{{\bf B}}
+\def\LBm{{\bf B}$^-$}
+\def\LBmi{{\bf B}$^-_{\limp}$}
+\def\LBmiq{{\bf B}$^-_{\limp\lexcl\lall\lex}$}
+\def\LBLS{{\bf BLS}}
+\def\P{{\cal P}}
+
+\def\mand{\mathrel{\textbf{and}}}
+\def\miff{\mathrel{\textbf{iff}}}
+\def\mimp{\mathrel{\textbf{implies}}}
+\def\mpiff{\mathrel{\textbf{\frenchspacing prim. iff}}}
+\def\mpimp{\mathrel{\textbf{\frenchspacing prim. implies}}}
+\def\mtrue{\mathord{\textbf{true}}}
+\def\mall{\mathrel{\textbf{all}}}
+
+% TEXT  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\def\EM#1{\noindent\hbox{\frenchspacing\em #1}}
+\def\TT#1{\noindent\hbox{\frenchspacing\tt #1}}
+\def\RM#1{\noindent\hbox{\frenchspacing\rm #1}}
+\def\URI#1{\texttt{<#1>}}
+
+\def\ie{{\frenchspacing i.e.}}
+\def\df#1{{\bf #1}}
+\long\def\xcomment#1{}
+\def\proc{{\frenchspacing proc.}}
+\def\etc{{\frenchspacing etc.}}
+\def\po{{\frenchspacing p.o.}}