src/Doc/ProgProve/Types_and_funs.thy
changeset 54605 cfdaa57ba67a
parent 54571 be1186cb03ce
child 55317 834a84553e02
--- 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}