--- a/src/Doc/IsarRef/Generic.thy Thu Nov 08 20:18:34 2012 +0100
+++ b/src/Doc/IsarRef/Generic.thy Thu Nov 08 20:20:38 2012 +0100
@@ -602,10 +602,10 @@
text {*
\begin{matharray}{rcl}
- @{command_def "print_simpset"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
@{attribute_def simp} & : & @{text attribute} \\
@{attribute_def split} & : & @{text attribute} \\
@{attribute_def cong} & : & @{text attribute} \\
+ @{command_def "print_simpset"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
\end{matharray}
@{rail "
@@ -615,21 +615,6 @@
\begin{description}
- \item @{command "print_simpset"} prints the collection of rules
- declared to the Simplifier, which is also known as ``simpset''
- internally.
-
- For historical reasons, simpsets may occur independently from the
- current context, but are conceptually dependent on it. When the
- Simplifier is invoked via one of its main entry points in the Isar
- source language (as proof method \secref{sec:simp-meth} or rule
- attribute \secref{sec:simp-meth}), its simpset is derived from the
- current proof context, and carries a back-reference to that for
- other tools that might get invoked internally (e.g.\ simplification
- procedures \secref{sec:simproc}). A mismatch of the context of the
- simpset and the context of the problem being simplified may lead to
- unexpected results.
-
\item @{attribute simp} declares rewrite rules, by adding or
deleting them from the simpset within the theory or proof context.
Rewrite rules are theorems expressing some form of equality, for
@@ -731,6 +716,21 @@
This can make simplification much faster, but may require an extra
case split over the condition @{text "?q"} to prove the goal.
+ \item @{command "print_simpset"} prints the collection of rules
+ declared to the Simplifier, which is also known as ``simpset''
+ internally.
+
+ For historical reasons, simpsets may occur independently from the
+ current context, but are conceptually dependent on it. When the
+ Simplifier is invoked via one of its main entry points in the Isar
+ source language (as proof method \secref{sec:simp-meth} or rule
+ attribute \secref{sec:simp-meth}), its simpset is derived from the
+ current proof context, and carries a back-reference to that for
+ other tools that might get invoked internally (e.g.\ simplification
+ procedures \secref{sec:simproc}). A mismatch of the context of the
+ simpset and the context of the problem being simplified may lead to
+ unexpected results.
+
\end{description}
The implicit simpset of the theory context is propagated