# HG changeset patch
# User nipkow
# Date 1366959705 -7200
# Node ID 89fb9f4abf84a92dffce7b239e262edcc4b4e07c
# Parent  f4a00cdae743c1244f0b9d33ebbcd62aafed358d
more funs

diff -r f4a00cdae743 -r 89fb9f4abf84 src/Doc/ProgProve/Logic.thy
--- 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
diff -r f4a00cdae743 -r 89fb9f4abf84 src/Doc/ProgProve/document/root.bib
--- 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}