doc-src/TutorialI/Misc/AdvancedInd.thy
changeset 10236 7626cb4e1407
parent 10217 e61e7e1eacaf
child 10241 e0428c2778f1
     1.1 --- a/doc-src/TutorialI/Misc/AdvancedInd.thy	Tue Oct 17 10:45:51 2000 +0200
     1.2 +++ b/doc-src/TutorialI/Misc/AdvancedInd.thy	Tue Oct 17 13:28:57 2000 +0200
     1.3 @@ -231,13 +231,17 @@
     1.4  identity.
     1.5  \end{exercise}
     1.6  
     1.7 -In general, @{text"induct_tac"} can be applied with any rule $r$
     1.8 +In general, @{text induct_tac} can be applied with any rule $r$
     1.9  whose conclusion is of the form ${?}P~?x@1 \dots ?x@n$, in which case the
    1.10  format is
    1.11  \begin{quote}
    1.12  \isacommand{apply}@{text"(induct_tac"} $y@1 \dots y@n$ @{text"rule:"} $r$@{text")"}
    1.13  \end{quote}\index{*induct_tac}%
    1.14  where $y@1, \dots, y@n$ are variables in the first subgoal.
    1.15 +A further example of a useful induction rule is @{thm[source]length_induct},
    1.16 +induction on the length of a list:\indexbold{*length_induct}
    1.17 +@{thm[display]length_induct[no_vars]}
    1.18 +
    1.19  In fact, @{text"induct_tac"} even allows the conclusion of
    1.20  $r$ to be an (iterated) conjunction of formulae of the above form, in
    1.21  which case the application is