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