src/Doc/ProgProve/Types_and_funs.thy
changeset 54605 cfdaa57ba67a
parent 54571 be1186cb03ce
child 55317 834a84553e02
equal deleted inserted replaced
54604:1512fa5fe531 54605:cfdaa57ba67a
   529 \isacom{apply}@{text"(simp split: nat.split)"}
   529 \isacom{apply}@{text"(simp split: nat.split)"}
   530 \end{quote}
   530 \end{quote}
   531 splits all case-expressions over natural numbers. For an arbitrary
   531 splits all case-expressions over natural numbers. For an arbitrary
   532 datatype @{text t} it is @{text "t.split"} instead of @{thm[source] nat.split}.
   532 datatype @{text t} it is @{text "t.split"} instead of @{thm[source] nat.split}.
   533 Method @{text auto} can be modified in exactly the same way.
   533 Method @{text auto} can be modified in exactly the same way.
       
   534 The modifier @{text "split:"} can be followed by multiple names.
       
   535 Splitting if or case-expressions in the assumptions requires 
       
   536 @{text "split: if_splits"} or @{text "split: t.splits"}.
   534 
   537 
   535 
   538 
   536 \subsection*{Exercises}
   539 \subsection*{Exercises}
   537 
   540 
   538 \exercise\label{exe:tree0}
   541 \exercise\label{exe:tree0}