diff -r ee42cba50933 -r e0825405d398 src/Doc/Isar_Ref/Preface.thy
--- a/src/Doc/Isar_Ref/Preface.thy	Mon Oct 12 21:42:14 2015 +0200
+++ b/src/Doc/Isar_Ref/Preface.thy	Mon Oct 12 22:03:24 2015 +0200
@@ -26,7 +26,8 @@
   Isabelle/jEdit Prover IDE @{cite "Wenzel:2012"} emphasizes the
   document-oriented approach of Isabelle/Isar again more explicitly.
 
-  \medskip Apart from the technical advances over bare-bones ML
+  \<^medskip>
+  Apart from the technical advances over bare-bones ML
   programming, the main purpose of the Isar language is to provide a
   conceptually different view on machine-checked proofs
   @{cite "Wenzel:1999:TPHOL" and "Wenzel-PhD"}.  \emph{Isar} stands for
@@ -49,7 +50,8 @@
   structured proofs.  Isabelle/Isar supports a broad range of proof
   styles, both readable and unreadable ones.
 
-  \medskip The generic Isabelle/Isar framework (see
+  \<^medskip>
+  The generic Isabelle/Isar framework (see
   \chref{ch:isar-framework}) works reasonably well for any Isabelle
   object-logic that conforms to the natural deduction view of the
   Isabelle/Pure framework.  Specific language elements introduced by
@@ -58,7 +60,8 @@
   framework, examples given in the generic parts will usually refer to
   Isabelle/HOL.
 
-  \medskip Isar commands may be either \emph{proper} document
+  \<^medskip>
+  Isar commands may be either \emph{proper} document
   constructors, or \emph{improper commands}.  Some proof methods and
   attributes introduced later are classified as improper as well.
   Improper Isar language elements, which are marked by ``@{text