%%%%%
%%%%%  THIS FILE MUST BE CALLED st.sty
%%%%%

\newtheorem{stdaxth}{A}
\newcommand{\stdax}[2]{\begin{stdaxth}\labelp{ax.#1} #2\end{stdaxth}}
\newtheorem{altaxth}{A}[stdaxth]
\newcommand{\altax}[2]{\begin{altaxth}\labelp{ax.#1} #2\end{altaxth}}

\newcommand{\axref}[1]{A\ref{ax.#1}}

\newtheorem{factaxth}{B}
\newcommand{\factax}[2]{\begin{factaxth}\labelp{ax.#1} #2\end{factaxth}}
\newtheorem{factaltaxth}{B}[factaxth]
\newcommand{\factaltax}[2]{\begin{factaltaxth}\labelp{ax.#1} #2\end{factaltaxth}}
\newcommand{\factaxref}[1]{B\ref{ax.#1}}

\newcommand{\rem}[1]{}


\newenvironment{pointer}{{\smallskip
{\bf  Pointers to the Literature\ }}
{\medskip}}

\newcommand{\fun}[3]{#1\colon #2\rightarrow #3}
\newcommand{\map}[3]{#1\colon #2\rightarrow #3}
\newcommand{\quadeq}{\quad = \quad}

\newcommand{\univ}[1]{|#1|}
\newcommand{\extn}[1]{\valof{#1}}
\newcommand{\ext}[2]{\extn{#1}^{#2}}
\newcommand{\relstr}[1]{[#1]}
\newcommand{\struct}[2]{\tuple{#1\; ;\; #2}}

\newcommand{\ob}[1]{{\sf #1}}
\newcommand{\obsmall}[1]{{\sf \scriptstyle #1}}
\newcommand{\Rel}{\ob{Rel}}
\newcommand{\Ass}{\ob{Ass}}
\newcommand{\Fun}{\ob{Fun}}
\newcommand{\Res}{\ob{Res}}
\newcommand{\Relation}{\ob{Relation}}
\newcommand{\ConjunctOf}{\ob{ConjunctOf}}
\newcommand{\DisjunctOf}{\ob{DisjunctOf}}
\newcommand{\NegatedBy}{\ob{NegatedBy}}
\newcommand{\zfm}{\ob{ZF}}
\newcommand{\Struct}{\ob{Struct}}
\newcommand{\Arg}{\ob{Arg}}
\newcommand{\Inf}{\ob{Inf}}
\newcommand{\Fact}{\ob{Fact}}
\newcommand{\Set}{\ob{Set}}
\newcommand{\Sit}{\ob{Sit}}
\newcommand{\HoldsIn}{\ob{HoldsIn}}
\newcommand{\SitOf}{\ob{SitOf}}
\newcommand{\InfOf}{\ob{InfOf}}
\newcommand{\Prop}{\ob{Prop}}
\newcommand{\True}{\ob{True}}
\newcommand{\Seq}{\ob{Seq}}
\newcommand{\Type}{\ob{Type}}
\newcommand{\Val}{\ob{Val}}
%\newcommand{\IS}[1]{\ob{IS}(#1)}


\newcommand{\rel}{\ob{rel}}
\newcommand{\ass}{\ob{ass}}
\newcommand{\inford}{\sqsubseteq}

\newcommand{\infon}[1]{\langle\!\langle\; #1\; \rangle\!\rangle}
\newcommand{\supports}{\vDash}
\newcommand{\nsupports}{\nvDash}
\newcommand{\implies}{\supset}
\newcommand{\spartof}{\sqsubseteq_s}
\newcommand{\partof}{\sqsubseteq}
\newcommand{\cpartof}{\sqsupseteq}
\newcommand{\scomp}{\smile_s}
\newcommand{\comp}{\smile}
\newcommand{\sunif}{\sqcup_s}
\newcommand{\ta}{\tau}


\newcommand{\inv}[1]{ #1^{-1}}
\newcommand{\res}[2]{#1\!\restriction\! #2}

\newcommand{\apr}[2]{(#1\supports #2)}
\newcommand{\pr}[2]{(#1\colon #2)}

\newcommand{\SInf}[1]{\mbox{SInf}(#1)}
\newcommand{\iSInf}[1]{\mbox{SInf}^-(#1)}
\newcommand{\lfSInf}[1]{\mbox{SInf}^*(#1)}
\newcommand{\ax}[2]{\enumsentence{\label{ax.#1} #2}}