# HG changeset patch
# User wenzelm
# Date 1446644418 -3600
# Node ID 26c76e143b77603e52c884b2e5055ca72cf20b8b
# Parent  e7d4dac7a79fff8631f32d67ef2c86165c1bd4ef
tuned;

diff -r e7d4dac7a79f -r 26c76e143b77 src/Doc/Isar_Ref/document/style.sty
--- 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}}
diff -r e7d4dac7a79f -r 26c76e143b77 src/Doc/System/Sessions.thy
--- 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>