src/HOL/Matrix/document/root.tex

added warning about inconsistent context to Metis;
it makes more sense here than in Sledgehammer, because Sledgehammer is unsound and there's no point in having people panicking about the consistency of their context when their context is in fact consistent

% $Id$

\documentclass[11pt,a4paper]{article}
\usepackage{isabelle,isabellesym}

% this should be the last package used
\usepackage{pdfsetup}

% urls in roman style, theory text in math-similar italics
\urlstyle{rm}
\isabellestyle{it}

\newcommand{\ganz}{\mathsf{Z}\mkern-7.5mu\mathsf{Z}}

\begin{document}

\title{Matrix}
\author{Steven Obua}
\maketitle

%\tableofcontents

\parindent 0pt\parskip 0.5ex

\input{session}

\end{document}