author | nipkow |

Sat Mar 27 18:43:11 2010 +0100 (2010-03-27) | |

changeset 35993 | 380b97496734 |

parent 35991 | 6ba552658807 |

parent 35992 | 78674c6018ca |

child 35994 | 9cc3df9a606e |

child 35995 | 26e820d27e0a |

merged

1.1 --- a/doc-src/TutorialI/Misc/document/simp.tex Sat Mar 27 18:12:02 2010 +0100 1.2 +++ b/doc-src/TutorialI/Misc/document/simp.tex Sat Mar 27 18:43:11 2010 +0100 1.3 @@ -653,13 +653,21 @@ 1.4 (recursive!) simplification of the conditions, the latter prefixed by 1.5 \texttt{[}$i+1$\texttt{]} instead of \texttt{[}$i$\texttt{]}. 1.6 Another source of recursive invocations of the simplifier are 1.7 -proofs of arithmetic formulae. 1.8 +proofs of arithmetic formulae. By default, recursive invocations are not shown, 1.9 +you must increase the trace depth via \pgmenu{Isabelle} $>$ \pgmenu{Settings} $>$ \pgmenu{Trace Simplifier Depth}. 1.10 1.11 Many other hints about the simplifier's actions may appear. 1.12 1.13 In more complicated cases, the trace can be very lengthy. Thus it is 1.14 advisable to reset the \pgmenu{Trace Simplifier} flag after having 1.15 -obtained the desired trace.% 1.16 +obtained the desired trace. 1.17 +% Since this is easily forgotten (and may have the unpleasant effect of 1.18 +% swamping the interface with trace information), here is how you can switch 1.19 +% the trace on locally: * } 1.20 +% 1.21 +%using [[trace_simp=true]] apply(simp) 1.22 +% In fact, any proof step can be prefixed with this \isa{using} clause, 1.23 +% causing any local simplification to be traced.% 1.24 \end{isamarkuptext}% 1.25 \isamarkuptrue% 1.26 %

2.1 --- a/doc-src/TutorialI/Misc/simp.thy Sat Mar 27 18:12:02 2010 +0100 2.2 +++ b/doc-src/TutorialI/Misc/simp.thy Sat Mar 27 18:43:11 2010 +0100 2.3 @@ -408,13 +408,22 @@ 2.4 (recursive!) simplification of the conditions, the latter prefixed by 2.5 \texttt{[}$i+1$\texttt{]} instead of \texttt{[}$i$\texttt{]}. 2.6 Another source of recursive invocations of the simplifier are 2.7 -proofs of arithmetic formulae. 2.8 +proofs of arithmetic formulae. By default, recursive invocations are not shown, 2.9 +you must increase the trace depth via \pgmenu{Isabelle} $>$ \pgmenu{Settings} $>$ \pgmenu{Trace Simplifier Depth}. 2.10 2.11 Many other hints about the simplifier's actions may appear. 2.12 2.13 In more complicated cases, the trace can be very lengthy. Thus it is 2.14 advisable to reset the \pgmenu{Trace Simplifier} flag after having 2.15 -obtained the desired trace. *} 2.16 +obtained the desired trace. 2.17 +% Since this is easily forgotten (and may have the unpleasant effect of 2.18 +% swamping the interface with trace information), here is how you can switch 2.19 +% the trace on locally: * } 2.20 +% 2.21 +%using [[trace_simp=true]] apply(simp) 2.22 +% In fact, any proof step can be prefixed with this \isa{using} clause, 2.23 +% causing any local simplification to be traced. 2.24 + *} 2.25 2.26 subsection{*Finding Theorems\label{sec:find}*} 2.27