changeset 15837 | 7a567dcd4cda |
parent 15763 | b901a127ac73 |
child 15995 | 251069032c03 |
--- a/doc-src/IsarRef/generic.tex Sat Apr 23 19:51:54 2005 +0200 +++ b/doc-src/IsarRef/generic.tex Mon Apr 25 17:58:41 2005 +0200 @@ -296,6 +296,12 @@ \end{descr} +\begin{warn} + Since attributes are applied to interpreted theorems, interpretation + may modify the current simpset and claset. Take this into + account when choosing attributes for local theorems. +\end{warn} + \section{Derived proof schemes}