--- a/src/Doc/Implementation/Eq.thy Wed Oct 14 15:06:42 2015 +0200
+++ b/src/Doc/Implementation/Eq.thy Wed Oct 14 15:10:32 2015 +0200
@@ -100,21 +100,21 @@
\begin{description}
- \item @{ML rewrite_rule}~@{text "ctxt rules thm"} rewrites the whole
+ \<^descr> @{ML rewrite_rule}~@{text "ctxt rules thm"} rewrites the whole
theorem by the given rules.
- \item @{ML rewrite_goals_rule}~@{text "ctxt rules thm"} rewrites the
+ \<^descr> @{ML rewrite_goals_rule}~@{text "ctxt rules thm"} rewrites the
outer premises of the given theorem. Interpreting the same as a
goal state (\secref{sec:tactical-goals}) it means to rewrite all
subgoals (in the same manner as @{ML rewrite_goals_tac}).
- \item @{ML rewrite_goal_tac}~@{text "ctxt rules i"} rewrites subgoal
+ \<^descr> @{ML rewrite_goal_tac}~@{text "ctxt rules i"} rewrites subgoal
@{text "i"} by the given rewrite rules.
- \item @{ML rewrite_goals_tac}~@{text "ctxt rules"} rewrites all subgoals
+ \<^descr> @{ML rewrite_goals_tac}~@{text "ctxt rules"} rewrites all subgoals
by the given rewrite rules.
- \item @{ML fold_goals_tac}~@{text "ctxt rules"} essentially uses @{ML
+ \<^descr> @{ML fold_goals_tac}~@{text "ctxt rules"} essentially uses @{ML
rewrite_goals_tac} with the symmetric form of each member of @{text
"rules"}, re-ordered to fold longer expression first. This supports
to idea to fold primitive definitions that appear in expended form