--- a/src/Doc/Isar_Ref/document/style.sty Wed Nov 04 11:53:22 2015 +0100
+++ b/src/Doc/Isar_Ref/document/style.sty Wed Nov 04 14:40:18 2015 +0100
@@ -40,8 +40,6 @@
\isabellestyle{literalunderscore}
-\newcommand{\isasymdash}{\isatext{\mbox{-}}}
-
\railtermfont{\isabellestyle{tt}}
\railnontermfont{\isabellestyle{literalunderscore}}
\railnamefont{\isabellestyle{literalunderscore}}
--- a/src/Doc/System/Sessions.thy Wed Nov 04 11:53:22 2015 +0100
+++ b/src/Doc/System/Sessions.thy Wed Nov 04 14:40:18 2015 +0100
@@ -145,8 +145,8 @@
text \<open>See @{file "~~/src/HOL/ROOT"} for a diversity of practically
relevant situations, although it uses relatively complex
- quasi-hierarchic naming conventions like \<open>HOL\<dash>SPARK\<close>,
- \<open>HOL\<dash>SPARK\<dash>Examples\<close>. An alternative is to use
+ quasi-hierarchic naming conventions like \<^verbatim>\<open>HOL-SPARK\<close>,
+ \<^verbatim>\<open>HOL-SPARK-Examples\<close>. An alternative is to use
unqualified names that are relatively long and descriptive, as in
the Archive of Formal Proofs (@{url "http://afp.sourceforge.net"}), for
example.\<close>