# HG changeset patch
# User nipkow
# Date 1385636677 -3600
# Node ID cfdaa57ba67a455f614bfbe4c6894131b5bd9c77
# Parent  1512fa5fe531f05fb1389ec864c9d7cbf0fe26f0
tuned

diff -r 1512fa5fe531 -r cfdaa57ba67a src/Doc/ProgProve/Types_and_funs.thy
--- a/src/Doc/ProgProve/Types_and_funs.thy	Thu Nov 28 08:35:14 2013 +0100
+++ b/src/Doc/ProgProve/Types_and_funs.thy	Thu Nov 28 12:04:37 2013 +0100
@@ -531,6 +531,9 @@
 splits all case-expressions over natural numbers. For an arbitrary
 datatype @{text t} it is @{text "t.split"} instead of @{thm[source] nat.split}.
 Method @{text auto} can be modified in exactly the same way.
+The modifier @{text "split:"} can be followed by multiple names.
+Splitting if or case-expressions in the assumptions requires 
+@{text "split: if_splits"} or @{text "split: t.splits"}.
 
 
 \subsection*{Exercises}