doc-src/TutorialI/fp.tex
 changeset 9689 751fde5307e4 parent 9673 1b2d4f995b13 child 9721 7e51c9f3d5a0
equal inserted replaced
9688:d1415164b814 9689:751fde5307e4
   532 simp $$list of modifiers$$
   532 simp $$list of modifiers$$
   533 \end{ttbox}
   533 \end{ttbox}
   534 where the list of \emph{modifiers} helps to fine tune the behaviour and may
   534 where the list of \emph{modifiers} helps to fine tune the behaviour and may
   535 be empty. Most if not all of the proofs seen so far could have been performed
   535 be empty. Most if not all of the proofs seen so far could have been performed
   536 with \isa{simp} instead of \isa{auto}, except that \isa{simp} attacks
   536 with \isa{simp} instead of \isa{auto}, except that \isa{simp} attacks
   537 only the first subgoal and may thus need to be repeated.
   537 only the first subgoal and may thus need to be repeated---use \isaindex{simp_all}

   538 to simplify all subgoals.
   538 Note that \isa{simp} fails if nothing changes.
   539 Note that \isa{simp} fails if nothing changes.
   539
   540
   540 \subsubsection{Adding and deleting simplification rules}
   541 \subsubsection{Adding and deleting simplification rules}
   541
   542
   542 If a certain theorem is merely needed in a few proofs by simplification,
   543 If a certain theorem is merely needed in a few proofs by simplification,
   849 \label{sec:recdef-induction}
   850 \label{sec:recdef-induction}
   850
   851
   851 \index{induction!recursion|)}
   852 \index{induction!recursion|)}
   852 \index{recursion induction|)}
   853 \index{recursion induction|)}
   853
   854
   854 %\subsection{Advanced forms of recursion}
   855 \subsection{Advanced forms of recursion}
   855
   856 \label{sec:advanced-recdef}
   856 %\input{Recdef/document/Nested0.tex}
   857
   857 %\input{Recdef/document/Nested1.tex}
   858 \input{Recdef/document/Nested0.tex}

   859 \input{Recdef/document/Nested1.tex}

   860 \input{Recdef/document/Nested2.tex}
   858
   861
   859 \index{*recdef|)}
   862 \index{*recdef|)}
   860
   863
   861 \section{Advanced induction techniques}
   864 \section{Advanced induction techniques}
   862 \label{sec:advanced-ind}
   865 \label{sec:advanced-ind}