equal
deleted
inserted
replaced
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} |