doc-src/TutorialI/fp.tex
 changeset 9742 98d3ca2c18f7 parent 9721 7e51c9f3d5a0 child 9754 a123a64cadeb
equal inserted replaced
9741:0502f06c2d29 9742:98d3ca2c18f7
   556 is proved by simplification, whereas the only slightly more complex
   556 is proved by simplification, whereas the only slightly more complex
   557
   557
   558 \input{Misc/document/arith4.tex}%
   558 \input{Misc/document/arith4.tex}%
   559 is not proved by simplification and requires \isa{arith}.
   559 is not proved by simplification and requires \isa{arith}.
   560
   560
   570 \subsubsection{Tracing}
   561 \subsubsection{Tracing}
   571 \indexbold{tracing the simplifier}
   562 \indexbold{tracing the simplifier}
   572
   563
   573 {\makeatother\input{Misc/document/trace_simp.tex}}
   564 {\makeatother\input{Misc/document/trace_simp.tex}}
   583
   565
   584 \index{simplification|)}
   566 \index{simplification|)}
   585
   567
   586 \section{Induction heuristics}
   568 \section{Induction heuristics}
   587 \label{sec:InductionHeuristics}
   569 \label{sec:InductionHeuristics}
   798 \input{Recdef/document/Nested0.tex}
   780 \input{Recdef/document/Nested0.tex}
   799 \input{Recdef/document/Nested1.tex}
   781 \input{Recdef/document/Nested1.tex}
   800 \input{Recdef/document/Nested2.tex}
   782 \input{Recdef/document/Nested2.tex}
   801
   783
   802 \index{*recdef|)}
   784 \index{*recdef|)}