\renewcommand{\topfraction}{1}
\renewcommand{\dbltopfraction}{1}
\renewcommand{\bottomfraction}{1}
\renewcommand{\textfraction}{0}

\renewcommand{\floatpagefraction}{.99} % for one-column
\renewcommand{\dblfloatpagefraction}{.99} % for two-.


%% macros for sample.tex

\usepackage{mathpartir}

%% metavariables

% types
\newmeta\s{s}              % these are automatically wrapped in \ma
\newmeta\t{t}

% expressions
\newmeta\M{M}
\newmeta\N{N}
\newmeta\P{P}
\newmeta\n{n}

% we write a macro for every bit of abstract syntax.  That way they
% will all look the same!

% types
\newbfop\any{any}
\newbfop\int{int}
\newbfop\bool{bool}
\newbfop\module{module}
\newbfop\true{true}
\newbfop\false{false}
\newbfop\blm{blame}
\newbfop\ifzero{if0}
\newcommand\dlsproctype[2]{(#1 \to #2)}
\newcommand\proccnt[2]{(#1 \to #2)}
% \proctype is a little overkill.
%% Reynolds' package can also abstract things like (\s1 \to \s2 \to \s3).

% terms
\newmeta\x{x}                   % not sure if \x is reserved...
\newmeta\c{c}
\newmeta\f{f}
\newmeta\e{e}
\newcommand\Tabs[3]{\ma{(\l #1 : #2 . #3)}}
\newcommand\dlsabs[2]{\ma{(\l #1 . #2)}}

% typing judgements
\newcommand\hastype[2]{\ma{#1 \mathbin{:} #2}}
\newcommand\typej[2]{\ma{\typejg{\Gamma}{#1}{#2}}}
\newcommand\typejg[3]{\ma{#1 \vdash \hastype{#2}{#3}}}

\newcommand\mtypej[3][P]{\ma{\mtypejg[#1]{\Gamma}{#2}{#3}}}
\newcommand\mtypejg[4][P]{\ma{\mtypejgp[#1]{#2}{#3}{#4}{}}}
\newcommand\mtypejgp[5][P]{\ma{#1, #2 \vdash^V_{#5} \hastype{#3}{#4}}}

\newcommand\subty[2]{\ma{#1 \mathbin{<:} #2}}

\newcommand\lift[1]{\ma{\lfloor #1 \rfloor}}

\newcommand\ifz[3]{(\ifzero\ #1\ #2\ #3)}


\newcommand\modu[2]{(\module\ #1\ #2)}
\newcommand\mc[3]{(\module\ #1\ #2\ #3)}
\newcommand\mt[3]{(\module\ #1\ #2\ #3)}

\newcommand\orcnt[2]{#1\ \vee\ #2}
\newcommand\cast[3]{\{#1 \Leftarrow^{#2} #3\}}
\newcommand\barrcnt[2]{(#1 \dashrightarrow #2)}

\newcommand\blame[1]{(\blm \ \ma{#1})}
\newcommand\redrule[3]{#1 & \longrightarrow & #2 & \mbox{\sc{#3}}}
\newcommand\redruletwoline[3]{{#1} & \longrightarrow &\multicolumn{2}{r}\mbox{\sc{#3}} \\ 
\multicolumn{2}{r}{#2}   & &   }

\newcommand\addcast[5]{P,#1 \vdash^{\Rightarrow} {\hastype{#2}{#3}} \rightsquigarrow #4 ; #5}
\newcommand\addcastg[4]{\addcast{\Gamma}{#1}{#2}{#3}{#4}}

\newcommand{\mathsmallest}[ 1]{\mbox{\scriptsize \ma{#1}}} 
\newcommand{\mathtiny}[1]{\mbox{\tiny\ma{#1}}}

\newcommand\ttproves[4]{P,#1 \vdash {\hastype{#2}{#3}} \rightsquigarrow #4}
\newcommand\ttgproves[3]{\ttproves{\Gamma}{#1}{#2}{#3}}

\newcommand\rtproves[4]{#1 \vdash^{\mathsmallest{RT}} {\hastype{#2}{#3}} ; #4}
\newcommand\rtgproves[3]{\rtproves{\Gamma}{#1}{#2}{#3}}

\newcommand\below{\triangleleft}

\newcommand\dlsreduces{\rightarrow^*}

\newcommand\merge[2]{\ma{merge(#1,#2)}}
\newcommand\mergetbl[3]{\ma{\merge{#1}{#2} &=& #3}}

\newcommand\context[1]{E[{\ma{#1}}]}

\newcommand\related[3][\ma{a}]{\ma{#2 \trianglerighteq_{#1} #3}}
\newcommand\similar[2]{\ma{#1 \triangleright #2}}

\newcommand\sth[1]{}
%\newcommand\qed[1]{}