src/Doc/How_to_Prove_it/document/root.tex
author wenzelm
Sun, 29 Sep 2024 15:00:20 +0200 (3 months ago)
changeset 80999 7f9e8516ca05
parent 73723 1bbbaae6b5e3
permissions -rw-r--r--
clarified input and output: support markup blocks via Bg/En; clarified datatype tree vs. tree_ops: reconstruct nested markup blocks via make_tree; clarified tree_ops_ord: ignore markup blocks, proceed like dict_ord;
\documentclass[11pt,a4paper]{report}

\input{prelude}

\begin{document}

\title{How to Prove it in Isabelle/HOL}
%\subtitle{\includegraphics[scale=.7]{isabelle_logo}}
\author{Tobias Nipkow}
\maketitle


\begin{abstract}
  How does one perform induction on the length of a list? How are numerals
  converted into \isa{Suc} terms? How does one prove equalities in rings
  and other algebraic structures?

  This document is a collection of practical hints and techniques for dealing
  with specific frequently occurring situations in proofs in Isabelle/HOL.
  Not arbitrary proofs but proofs that refer to material that is part of
  \isa{Main} or \isa{Complex\_Main}.

  This is \emph{not} an introduction to
\begin{itemize}
\item proofs in general; for that see mathematics or logic books.
\item Isabelle/HOL and its proof language; for that see the tutorial
  \cite{ProgProve} or the reference manual~\cite{IsarRef}.
\item the contents of theory \isa{Main}; for that see the overview
  \cite{Main}.
\end{itemize}
\end{abstract}

\setcounter{tocdepth}{1}
\tableofcontents

\input{How_to_Prove_it.tex}

\bibliographystyle{plain}
\bibliography{root}

%\printindex

\end{document}