equal
deleted
inserted
replaced
47 are invented by Isabelle and have nothing to do with the names in the |
47 are invented by Isabelle and have nothing to do with the names in the |
48 definition of \isa{sep}. |
48 definition of \isa{sep}. |
49 |
49 |
50 In general, the format of invoking recursion induction is |
50 In general, the format of invoking recursion induction is |
51 \begin{quote} |
51 \begin{quote} |
52 \isacommand{apply}\isa{{\isacharparenleft}induct{\isacharunderscore}tac\ }$x@1 \dots x@n$ \isa{rule{\isacharcolon}} $f$\isa{{\isachardot}induct{\isacharparenright}} |
52 \isacommand{apply}\isa{{\isacharparenleft}induct{\isacharunderscore}tac}$x@1 \dots x@n$ \isa{rule{\isacharcolon}} $f$\isa{{\isachardot}induct{\isacharparenright}} |
53 \end{quote}\index{*induct_tac}% |
53 \end{quote}\index{*induct_tac}% |
54 where $x@1~\dots~x@n$ is a list of free variables in the subgoal and $f$ the |
54 where $x@1~\dots~x@n$ is a list of free variables in the subgoal and $f$ the |
55 name of a function that takes an $n$-tuple. Usually the subgoal will |
55 name of a function that takes an $n$-tuple. Usually the subgoal will |
56 contain the term $f(x@1,\dots,x@n)$ but this need not be the case. The |
56 contain the term $f(x@1,\dots,x@n)$ but this need not be the case. The |
57 induction rules do not mention $f$ at all. For example \isa{sep{\isachardot}induct} |
57 induction rules do not mention $f$ at all. For example \isa{sep{\isachardot}induct} |