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 repeateduse \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:recdefinduction} 
850 \label{sec:recdefinduction} 
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:advancedrecdef} 
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:advancedind} 
865 \label{sec:advancedind} 