
diff -r 151f894984d8 -r 2bf52eec4e8a src/Doc/Implementation/Eq.thy
--- 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




