\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}
¤ Dauer der Verarbeitung: 0.2 Sekunden
(vorverarbeitet)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
