--- a/src/Doc/ProgProve/Logic.thy Fri Apr 26 07:49:38 2013 +0200
+++ b/src/Doc/ProgProve/Logic.thy Fri Apr 26 09:01:45 2013 +0200
@@ -105,6 +105,20 @@
Sets also allow bounded quantifications @{prop"ALL x : A. P"} and
@{prop"EX x : A. P"}.
+Some more frequently useful functions on sets:
+\begin{center}
+\begin{tabular}{ll}
+@{const_typ set} & converts a list to the set of its elements\\
+@{const_typ finite} & is true iff its argument is finite\\
+@{const_typ card} & is the cardinality of a finite set\\
+ & and is @{text 0} for all infinite sets\\
+@{thm image_def} & is the image of a function over a set
+\end{tabular}
+\end{center}
+
+See \cite{Nipkow-Main} for the wealth of further predefined functions in theory
+@{theory Main}.
+
\section{Proof automation}
So far we have only seen @{text simp} and @{text auto}: Both perform
--- a/src/Doc/ProgProve/document/root.bib Fri Apr 26 07:49:38 2013 +0200
+++ b/src/Doc/ProgProve/document/root.bib Fri Apr 26 09:01:45 2013 +0200
@@ -9,6 +9,9 @@
title={Defining Recursive Functions in Isabelle/HOL},
note={\url{http://isabelle.in.tum.de/doc/functions.pdf}}}
+@manual{Nipkow-Main,author={Tobias Nipkow},title={What's in Main},
+note={\url{http://isabelle.in.tum.de/doc/main.pdf}}}
+
@book{LNCS2283,author={Tobias Nipkow and Lawrence Paulson and Markus Wenzel},
title="Isabelle/HOL --- A Proof Assistant for Higher-Order Logic",
publisher=Springer,series=LNCS,volume=2283,year=2002}