--- a/src/Doc/Eisbach/Preface.thy Sat Jan 05 17:00:43 2019 +0100
+++ b/src/Doc/Eisbach/Preface.thy Sat Jan 05 17:24:33 2019 +0100
@@ -32,9 +32,8 @@
well as the @{method match} method, as well as discussing their integration
with existing Isar concepts such as @{command named_theorems}.
- These commands are provided by theory @{theory "HOL-Eisbach.Eisbach"}: it
- needs to be imported by all Eisbach applications. Theory theory @{theory
- "HOL-Eisbach.Eisbach_Tools"} provides additional proof methods and
+ These commands are provided by theory \<^theory>\<open>HOL-Eisbach.Eisbach\<close>: it
+ needs to be imported by all Eisbach applications. Theory theory \<^theory>\<open>HOL-Eisbach.Eisbach_Tools\<close> provides additional proof methods and
attributes that are occasionally useful.
\<close>