
% Use inter-paragraph spacing rather than indenting the start of each
% paragraph. Works better with many very short paragraphs.
\usepackage{parskip}

\usepackage{a4wide}
\usepackage{graphics}
\usepackage{mathtools}
\usepackage{stmaryrd}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{wasysym}
\usepackage{mathrsfs}
\usepackage{calc}
\usepackage{forloop}

\usepackage{color}
\usepackage{framed}
\definecolor{shadecolor}{rgb}{0.7,1,0.7}

% This makes << etc in coq sections readable.
% You need cm-super fonts installed (cm-super package in Debian), or it
% won't look good, and you will get lots of
%     Error: Bad bounding box in Type 3 glyph
% errors.
\usepackage[T1]{fontenc}

\usepackage{coqdoc}
\renewcommand{\coqlibrary}[2]{}
\renewenvironment{coqdoccode}{\shaded}{\endshaded}

\newenvironment{igpic}{\definecolor{shadecolor}{rgb}{0.9,0.9,0.9}\shaded\begin{mfpic}}{\end{mfpic}\endshaded}

% For axiom etc
\usepackage[amsmath,thmmarks]{ntheorem}
{
\theoremstyle{break}
\theorembodyfont{\rmfamily}
\theoremindent0.5cm
\newtheorem{Iaxiom}{Axiom}[section]
\newtheorem{Ilemma}{Lemma}[section]
\newtheorem{Iconjecture}{Conjecture}[section]
\newtheorem{Itheorem}{Theorem}[section]
\newtheorem{Idefinition}{Definition}[section]
\theoremstyle{nonumberbreak}
%\theoremindent0cm
\theoremsymbol{\rule{1ex}{1ex}}
\newtheorem{Iproof}{Proof}
\theoremsymbol{}
\theorembodyfont{\itshape}
\newtheorem{Iaside}{Aside}
\newtheorem{Iexplanation}{Explanation}
}
% \newenvironment{axiom}[1]{\par\noindent\textbf{Axiom}: {#1}\par}{}
\newenvironment{rationale}{\par\noindent\textbf{Rationale}\par}{}
\setlength{\theorempreskipamount}{\bigskipamount}
% Use \start{axiom}{name} rather than \begin{Iaxiom}[name], and get a
% axiom:name label for free!
\newcommand{\start}[2]{\begin{I#1}[#2]\label{#1:#2}}

\newcommand{\refAxiom}[1]{Axiom~\ref{axiom:#1}}
\newcommand{\refLemma}[1]{Lemma~\ref{lemma:#1}}
\newcommand{\refSection}[1]{Section~\ref{sec:#1}}
\newcommand{\refAppendix}[1]{Appendix~\ref{sec:#1}}
\newcommand{\refDefinition}[1]{Definition~\ref{definition:#1}}

\input{mathlig}

\setlength{\overfullrule}{2pt}    % Highlights overfull boxes in the printout
\showboxdepth=3\showboxbreadth=99 % makes overfull warnings clearer.

\newcommand{\ourstrut}{\vphantom{j}}

\newcommand{\inverted}{{^{-1}}}
\newcommand{\seq}[1]{\overline{\ourstrut #1}}
\newcommand{\unnamed}[1]{\underline{\ourstrut #1}}

\newcommand{\ie}{i.e.\null}
\newcommand{\eg}{e.g.\null}
\newcommand{\abetc}{etc.\null}

\newcommand{\qqqquad}{\qquad\qquad}

