equal
deleted
inserted
replaced
84 \S\ref{sec:reordering-asms} for ways around this problem. |
84 \S\ref{sec:reordering-asms} for ways around this problem. |
85 \end{warn} |
85 \end{warn} |
86 |
86 |
87 Using the simplifier effectively may take a bit of experimentation. |
87 Using the simplifier effectively may take a bit of experimentation. |
88 \index{tracing!of simplification}\index{*trace_simp} The tactics can |
88 \index{tracing!of simplification}\index{*trace_simp} The tactics can |
89 be traced by setting \verb$trace_simp := true$. |
89 be traced by setting \verb$trace_simp$. |
90 |
90 |
91 There is not just one global current simpset, but one associated with each |
91 There is not just one global current simpset, but one associated with each |
92 theory as well. How are these simpset built up? |
92 theory as well. How are these simpset built up? |
93 \begin{enumerate} |
93 \begin{enumerate} |
94 \item When loading {\tt T.thy}, the current simpset is initialized with the |
94 \item When loading {\tt T.thy}, the current simpset is initialized with the |