doc-src/TutorialI/fp.tex
changeset 9689 751fde5307e4
parent 9673 1b2d4f995b13
child 9721 7e51c9f3d5a0
equal deleted 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}