%% Style file for Community Z Tools (CZT) Project.
  %% This extends oz.sty, which defines all the symbols we need
  %% and seems to be widely available.
  
  \usepackage{oz}
  
  % Some standard Z commands
  
  ewenvironment{zsection}{\zed}{\endzed}
  
  ewcommand{\SECTION}{\boldword{section}}
  
  ewcommand{\parents}{\boldword{parents}}
  
  ewcommand{\function}{\boldword{function}}
  
  ewcommand{\generic}{\boldword{generic}}
  
  ewcommand{\relation}{\boldword{relation}}
  
  ewcommand{\leftassoc}{\boldword{leftassoc}}
  
  ewcommand{\rightassoc}{\boldword{rightassoc}}
  
  ewcommand{\LET}{\boldword{let}}
  
  ewcommand{\IF}{\boldword{if}}
  
  ewcommand{\THEN}{\boldword{then}}
  
  ewcommand{\ELSE}{\boldword{else}}
  
  %% These need defining, because they are not defined in oz.sty
  
  ewcommand{\listarg}{\mathrel{,,}}
  
  ewcommand{\varg}{\mathbin{\_}}
  
  ewcommand{\symdiff}{\mathbin{\ominus}}
  
  ewcommand{\plus}{{}^{+}}
  
  ewcommand{\extract}{\mathbin{\ires}}  % \ires is from oz.sty
  
  ewcommand{
  egate}{\mathop{-}}
  
  ewcommand{\arithmos}{{\mathbb A}}  % oz.sty loads the AMS fonts
  
  ewcommand{\pipe}{\zpipe}           % \zpipe is from oz.sty
  
  %% These need redefining, because the Z standard requires
  %% something different to oz.sty (or to LaTeX, for \star!)
  \def\star{{}^{*}}   % we must override standard LaTeX \star! 
  \def\infix{\boldword{infix}}          % this overrides the oz.sty \infix.
  \def\partition{\boldword{partition}}  % overrides the oz.sty 'partitions'
  
  %% The Z Standard now uses the 'theorem' environment for conjectures.
  %% See the Z Standard defect report 13568/003,
  %% available from http://www.cs.york.ac.uk/hise/Zstandard/defects.html
  %% Here are several different styles for displaying the theorem name:
  %% As a zero-width superscript
  %
  ewcommand{\ZedTheoremName}[1]{\hbox to
  %        0pt{\raisebox{2ex}{\scriptsize#1}}}
  %% As a left-margin annotation
  
  ewcommand{\ZedTheoremName}[1]{\llap{\raisebox{0.0ex}{%
        \scriptsize#1\hspace{0.5em}}}}
  %% Like a right-justified equation number
  %
  ewcommand{\ZedTheoremName}[1]{\hbox to 0pt{\hbox to
  %    \textwidth{\hbox{}\hfill{\footnotesize[#1]}}}} 
  %% Do not show it at all.
  %
  ewcommand{\ZedTheoremName}[1]{}
  \renewenvironment{theorem}[1]{\zed\ZedTheoremName{#1}}{\endzed}
  
  
  %% These commands are for the ZPattern extension of Z,
  %% which makes it possible to define rewrite rules and inference rules.
  %% See zpattern_toolkit.tex for the Z-parseable parts of the definitions.
  
  
  ewenvironment{zedjoker}[1]{\par$\bigstar$ #1\ }{\hfill\par}
  
  % Rule syntax: \begin{zedrule}{Name} Ant1 \\ Ant2 \derive Concl \end{zedrule}
  
  ewenvironment{zedrule}[1]{\par\textbf{rule }#1\vspace{-2ex}\infrule}{\endinfrule}
  
  ewcommand{\derives}{\derive{}}
  
  ewcommand{\substitute}{\mathrel{\curvearrowleft}}  % U+21B6
  
  ewcommand{\proviso}{\raisebox{0.5ex}{${}_{\blacktriangleright}\ $}}%%or\star
  %       This mapping to unicode is now in zpattern_toolkit.tex
  %       %%Zprechar \proviso U+22C6    % small star, or
  %       %%Zprechar \proviso U+25B8    % small solid triangle  |> )
  
  % Z Pattern operators for use within == provisos.
  
  ewcommand{\schemaminus}{\mathbin{\textbf{schemaminus}}}
  
  ewcommand{\schemamerge}{\mathbin{\textbf{schemamerge}}}
  
  ewcommand{\hasDefn}{\mathbin{\textbf{hasDefn}}}
  
  ewcommand{\is}{\mathbin{\textbf{is}}}
  
  % These Z Pattern operators are not used yet.
  
  ewcommand{\Context}{\Gamma}
  
  ewcommand{
  otfreein}{\mathbin{\boldword{notfreein}}}