src/Doc/System/Sessions.thy
changeset 63680 6e1e8b5abbfa
parent 63669 256fc20716f2
child 63827 b24d0e53dd03
--- a/src/Doc/System/Sessions.thy	Fri Aug 12 17:49:02 2016 +0200
+++ b/src/Doc/System/Sessions.thy	Fri Aug 12 17:53:55 2016 +0200
@@ -140,19 +140,18 @@
 subsubsection \<open>Examples\<close>
 
 text \<open>
-  See @{file "~~/src/HOL/ROOT"} for a diversity of practically relevant
-  situations, although it uses relatively complex 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.
+  See \<^file>\<open>~~/src/HOL/ROOT\<close> for a diversity of practically relevant situations,
+  although it uses relatively complex 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>\<open>http://afp.sourceforge.net\<close>), for example.
 \<close>
 
 
 section \<open>System build options \label{sec:system-options}\<close>
 
 text \<open>
-  See @{file "~~/etc/options"} for the main defaults provided by the Isabelle
+  See \<^file>\<open>~~/etc/options\<close> for the main defaults provided by the Isabelle
   distribution. Isabelle/jEdit @{cite "isabelle-jedit"} includes a simple
   editing mode \<^verbatim>\<open>isabelle-options\<close> for this file-format.