more symbols;
authorwenzelm
Fri Aug 12 17:53:55 2016 +0200 (2016-08-12)
changeset 636806e1e8b5abbfa
parent 63679 dc311d55ad8f
child 63681 d2448471ffba
more symbols;
src/Doc/Codegen/Adaptation.thy
src/Doc/Codegen/Further.thy
src/Doc/Codegen/Inductive_Predicate.thy
src/Doc/Corec/Corec.thy
src/Doc/Datatypes/Datatypes.thy
src/Doc/Implementation/Eq.thy
src/Doc/Implementation/Integration.thy
src/Doc/Implementation/Logic.thy
src/Doc/Implementation/ML.thy
src/Doc/Implementation/Tactic.thy
src/Doc/Isar_Ref/Document_Preparation.thy
src/Doc/Isar_Ref/Framework.thy
src/Doc/Isar_Ref/HOL_Specific.thy
src/Doc/Isar_Ref/Inner_Syntax.thy
src/Doc/Isar_Ref/Spec.thy
src/Doc/Isar_Ref/Synopsis.thy
src/Doc/JEdit/JEdit.thy
src/Doc/Locales/Examples3.thy
src/Doc/Main/Main_Doc.thy
src/Doc/Prog_Prove/Basics.thy
src/Doc/System/Environment.thy
src/Doc/System/Misc.thy
src/Doc/System/Presentation.thy
src/Doc/System/Scala.thy
src/Doc/System/Sessions.thy
src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
src/HOL/Analysis/Linear_Algebra.thy
src/HOL/Bali/Decl.thy
src/HOL/Binomial.thy
src/HOL/Groups.thy
src/HOL/HOLCF/IOA/RefCorrectness.thy
src/HOL/HOLCF/IOA/Traces.thy
src/HOL/Imperative_HOL/Ref.thy
src/HOL/Induct/Ordinals.thy
src/HOL/Isar_Examples/Cantor.thy
src/HOL/Isar_Examples/Hoare.thy
src/HOL/Isar_Examples/Schroeder_Bernstein.thy
src/HOL/Library/Code_Test.thy
src/HOL/Library/Extended_Real.thy
src/HOL/Library/RBT_Impl.thy
src/HOL/Library/Set_Algebras.thy
src/HOL/Library/State_Monad.thy
src/HOL/Nominal/Examples/CK_Machine.thy
src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy
src/HOL/Probability/Probability_Mass_Function.thy
src/HOL/Real.thy
src/HOL/Real_Vector_Spaces.thy
src/HOL/Rings.thy
src/HOL/Series.thy
src/HOL/Tools/Quickcheck/narrowing_generators.ML
src/HOL/Word/Word.thy
src/HOL/ex/ML.thy
src/HOL/ex/NatSum.thy
src/HOL/ex/Simproc_Tests.thy
src/HOL/ex/Sudoku.thy
src/Pure/Tools/jedit.ML
     1.1 --- a/src/Doc/Codegen/Adaptation.thy	Fri Aug 12 17:49:02 2016 +0200
     1.2 +++ b/src/Doc/Codegen/Adaptation.thy	Fri Aug 12 17:53:55 2016 +0200
     1.3 @@ -154,7 +154,7 @@
     1.4    The @{theory HOL} @{theory Main} theory already provides a code
     1.5    generator setup which should be suitable for most applications.
     1.6    Common extensions and modifications are available by certain
     1.7 -  theories in @{dir "~~/src/HOL/Library"}; beside being useful in
     1.8 +  theories in \<^dir>\<open>~~/src/HOL/Library\<close>; beside being useful in
     1.9    applications, they may serve as a tutorial for customising the code
    1.10    generator setup (see below \secref{sec:adaptation_mechanisms}).
    1.11  
     2.1 --- a/src/Doc/Codegen/Further.thy	Fri Aug 12 17:49:02 2016 +0200
     2.2 +++ b/src/Doc/Codegen/Further.thy	Fri Aug 12 17:53:55 2016 +0200
     2.3 @@ -148,7 +148,7 @@
     2.4  subsection \<open>Parallel computation\<close>
     2.5  
     2.6  text \<open>
     2.7 -  Theory @{text Parallel} in @{dir "~~/src/HOL/Library"} contains
     2.8 +  Theory @{text Parallel} in \<^dir>\<open>~~/src/HOL/Library\<close> contains
     2.9    operations to exploit parallelism inside the Isabelle/ML
    2.10    runtime engine.
    2.11  \<close>
     3.1 --- a/src/Doc/Codegen/Inductive_Predicate.thy	Fri Aug 12 17:49:02 2016 +0200
     3.2 +++ b/src/Doc/Codegen/Inductive_Predicate.thy	Fri Aug 12 17:53:55 2016 +0200
     3.3 @@ -262,7 +262,7 @@
     3.4  
     3.5  text \<open>
     3.6    Further examples for compiling inductive predicates can be found in
     3.7 -  @{file "~~/src/HOL/Predicate_Compile_Examples/Examples.thy"}.  There are
     3.8 +  \<^file>\<open>~~/src/HOL/Predicate_Compile_Examples/Examples.thy\<close>.  There are
     3.9    also some examples in the Archive of Formal Proofs, notably in the
    3.10    @{text "POPLmark-deBruijn"} and the @{text "FeatherweightJava"}
    3.11    sessions.
     4.1 --- a/src/Doc/Corec/Corec.thy	Fri Aug 12 17:49:02 2016 +0200
     4.2 +++ b/src/Doc/Corec/Corec.thy	Fri Aug 12 17:53:55 2016 +0200
     4.3 @@ -22,7 +22,7 @@
     4.4  text \<open>
     4.5  Isabelle's (co)datatype package @{cite "isabelle-datatypes"} offers a convenient
     4.6  syntax for introducing codatatypes. For example, the type of (infinite) streams
     4.7 -can be defined as follows (cf. @{file "~~/src/HOL/Library/Stream.thy"}):
     4.8 +can be defined as follows (cf. \<^file>\<open>~~/src/HOL/Library/Stream.thy\<close>):
     4.9  \<close>
    4.10  
    4.11      codatatype 'a stream =
    4.12 @@ -38,7 +38,7 @@
    4.13  @{command corecursive}, @{command friend_of_corec}, and @{command coinduction_upto}.
    4.14  It also covers the @{method corec_unique} proof method.
    4.15  The package is not part of @{theory Main}; it is located in
    4.16 -@{file "~~/src/HOL/Library/BNF_Corec.thy"}.
    4.17 +\<^file>\<open>~~/src/HOL/Library/BNF_Corec.thy\<close>.
    4.18  
    4.19  The @{command corec} command generalizes \keyw{primcorec} in three main
    4.20  respects. First, it allows multiple constructors around corecursive calls, where
    4.21 @@ -127,7 +127,7 @@
    4.22  text \<open>
    4.23  The package is illustrated through concrete examples featuring different flavors
    4.24  of corecursion. More examples can be found in the directory
    4.25 -@{dir "~~/src/HOL/Corec_Examples"}.
    4.26 +\<^dir>\<open>~~/src/HOL/Corec_Examples\<close>.
    4.27  \<close>
    4.28  
    4.29  
    4.30 @@ -368,7 +368,7 @@
    4.31  
    4.32  text \<open>
    4.33  A more elaborate case study, revolving around the filter function on lazy lists,
    4.34 -is presented in @{file "~~/src/HOL/Corec_Examples/LFilter.thy"}.
    4.35 +is presented in \<^file>\<open>~~/src/HOL/Corec_Examples/LFilter.thy\<close>.
    4.36  \<close>
    4.37  
    4.38  
     5.1 --- a/src/Doc/Datatypes/Datatypes.thy	Fri Aug 12 17:49:02 2016 +0200
     5.2 +++ b/src/Doc/Datatypes/Datatypes.thy	Fri Aug 12 17:53:55 2016 +0200
     5.3 @@ -78,7 +78,7 @@
     5.4  infinite branching.
     5.5  
     5.6  The package is part of @{theory Main}. Additional functionality is provided by
     5.7 -the theory @{file "~~/src/HOL/Library/BNF_Axiomatization.thy"}.
     5.8 +the theory \<^file>\<open>~~/src/HOL/Library/BNF_Axiomatization.thy\<close>.
     5.9  
    5.10  The package, like its predecessor, fully adheres to the LCF philosophy
    5.11  @{cite mgordon79}: The characteristic theorems associated with the specified
    5.12 @@ -163,7 +163,7 @@
    5.13  text \<open>
    5.14  Datatypes are illustrated through concrete examples featuring different flavors
    5.15  of recursion. More examples can be found in the directory
    5.16 -@{dir "~~/src/HOL/Datatype_Examples"}.
    5.17 +\<^dir>\<open>~~/src/HOL/Datatype_Examples\<close>.
    5.18  \<close>
    5.19  
    5.20  
    5.21 @@ -1138,7 +1138,7 @@
    5.22    \label{sssec:datatype-compat}\<close>
    5.23  
    5.24  text \<open>
    5.25 -The theory @{file "~~/src/HOL/Library/Countable.thy"} provides a
    5.26 +The theory \<^file>\<open>~~/src/HOL/Library/Countable.thy\<close> provides a
    5.27  proof method called @{method countable_datatype} that can be used to prove the
    5.28  countability of many datatypes, building on the countability of the types
    5.29  appearing in their definitions and of any type arguments. For example:
    5.30 @@ -1218,7 +1218,7 @@
    5.31  \end{itemize}
    5.32  
    5.33  The old command is still available as \keyw{old_datatype} in theory
    5.34 -@{file "~~/src/HOL/Library/Old_Datatype.thy"}. However, there is no general
    5.35 +\<^file>\<open>~~/src/HOL/Library/Old_Datatype.thy\<close>. However, there is no general
    5.36  way to register old-style datatypes as new-style datatypes. If the objective
    5.37  is to define new-style datatypes with nested recursion through old-style
    5.38  datatypes, the old-style datatypes can be registered as a BNF
    5.39 @@ -1247,7 +1247,7 @@
    5.40  text \<open>
    5.41  Primitive recursion is illustrated through concrete examples based on the
    5.42  datatypes defined in Section~\ref{ssec:datatype-introductory-examples}. More
    5.43 -examples can be found in the directory @{dir "~~/src/HOL/Datatype_Examples"}.
    5.44 +examples can be found in the directory \<^dir>\<open>~~/src/HOL/Datatype_Examples\<close>.
    5.45  \<close>
    5.46  
    5.47  
    5.48 @@ -1320,7 +1320,7 @@
    5.49  Pattern matching is only available for the argument on which the recursion takes
    5.50  place. Fortunately, it is easy to generate pattern-maching equations using the
    5.51  @{command simps_of_case} command provided by the theory
    5.52 -@{file "~~/src/HOL/Library/Simps_Case_Conv.thy"}.
    5.53 +\<^file>\<open>~~/src/HOL/Library/Simps_Case_Conv.thy\<close>.
    5.54  \<close>
    5.55  
    5.56      simps_of_case at_simps_alt: at.simps
    5.57 @@ -1760,7 +1760,7 @@
    5.58  Codatatypes can be specified using the @{command codatatype} command. The
    5.59  command is first illustrated through concrete examples featuring different
    5.60  flavors of corecursion. More examples can be found in the directory
    5.61 -@{dir "~~/src/HOL/Datatype_Examples"}. The \emph{Archive of Formal Proofs} also
    5.62 +\<^dir>\<open>~~/src/HOL/Datatype_Examples\<close>. The \emph{Archive of Formal Proofs} also
    5.63  includes some useful codatatypes, notably for lazy lists @{cite
    5.64  "lochbihler-2010"}.
    5.65  \<close>
    5.66 @@ -2038,7 +2038,7 @@
    5.67  on @{command primcorec} and @{command primcorecursive}; \keyw{corec} and
    5.68  \keyw{corecursive} are described in a separate tutorial
    5.69  @{cite "isabelle-corec"}. More examples can be found in the directories
    5.70 -@{dir "~~/src/HOL/Datatype_Examples"} and @{dir "~~/src/HOL/Corec_Examples"}.
    5.71 +\<^dir>\<open>~~/src/HOL/Datatype_Examples\<close> and \<^dir>\<open>~~/src/HOL/Corec_Examples\<close>.
    5.72  
    5.73  Whereas recursive functions consume datatypes one constructor at a time,
    5.74  corecursive functions construct codatatypes one constructor at a time.
    5.75 @@ -2082,7 +2082,7 @@
    5.76  text \<open>
    5.77  Primitive corecursion is illustrated through concrete examples based on the
    5.78  codatatypes defined in Section~\ref{ssec:codatatype-introductory-examples}. More
    5.79 -examples can be found in the directory @{dir "~~/src/HOL/Datatype_Examples"}.
    5.80 +examples can be found in the directory \<^dir>\<open>~~/src/HOL/Datatype_Examples\<close>.
    5.81  The code view is favored in the examples below. Sections
    5.82  \ref{ssec:primrec-constructor-view} and \ref{ssec:primrec-destructor-view}
    5.83  present the same examples expressed using the constructor and destructor views.
    5.84 @@ -2143,7 +2143,7 @@
    5.85  
    5.86  Pattern matching is not supported by @{command primcorec}. Fortunately, it is
    5.87  easy to generate pattern-maching equations using the @{command simps_of_case}
    5.88 -command provided by the theory @{file "~~/src/HOL/Library/Simps_Case_Conv.thy"}.
    5.89 +command provided by the theory \<^file>\<open>~~/src/HOL/Library/Simps_Case_Conv.thy\<close>.
    5.90  \<close>
    5.91  
    5.92      simps_of_case lapp_simps: lapp.code
    5.93 @@ -2776,7 +2776,7 @@
    5.94  text \<open>
    5.95  The example below shows how to register a type as a BNF using the @{command bnf}
    5.96  command. Some of the proof obligations are best viewed with the theory
    5.97 -@{file "~~/src/HOL/Library/Cardinal_Notations.thy"} imported.
    5.98 +\<^file>\<open>~~/src/HOL/Library/Cardinal_Notations.thy\<close> imported.
    5.99  
   5.100  The type is simply a copy of the function space @{typ "'d \<Rightarrow> 'a"}, where @{typ 'a}
   5.101  is live and @{typ 'd} is dead. We introduce it together with its map function,
   5.102 @@ -2875,10 +2875,10 @@
   5.103  
   5.104  This particular example does not need any nonemptiness witness, because the
   5.105  one generated by default is good enough, but in general this would be
   5.106 -necessary. See @{file "~~/src/HOL/Basic_BNFs.thy"},
   5.107 -@{file "~~/src/HOL/Library/Countable_Set_Type.thy"},
   5.108 -@{file "~~/src/HOL/Library/FSet.thy"}, and
   5.109 -@{file "~~/src/HOL/Library/Multiset.thy"} for further examples of BNF
   5.110 +necessary. See \<^file>\<open>~~/src/HOL/Basic_BNFs.thy\<close>,
   5.111 +\<^file>\<open>~~/src/HOL/Library/Countable_Set_Type.thy\<close>,
   5.112 +\<^file>\<open>~~/src/HOL/Library/FSet.thy\<close>, and
   5.113 +\<^file>\<open>~~/src/HOL/Library/Multiset.thy\<close> for further examples of BNF
   5.114  registration, some of which feature custom witnesses.
   5.115  
   5.116  For many typedefs, lifting the BNF structure from the raw type to the abstract
   5.117 @@ -3107,7 +3107,7 @@
   5.118  
   5.119  The command is useful to reason abstractly about BNFs. The axioms are safe
   5.120  because there exist BNFs of arbitrary large arities. Applications must import
   5.121 -the @{file "~~/src/HOL/Library/BNF_Axiomatization.thy"} theory
   5.122 +the \<^file>\<open>~~/src/HOL/Library/BNF_Axiomatization.thy\<close> theory
   5.123  to use this functionality.
   5.124  \<close>
   5.125  
   5.126 @@ -3210,7 +3210,7 @@
   5.127  
   5.128  \noindent
   5.129  The @{command simps_of_case} command provided by theory
   5.130 -@{file "~~/src/HOL/Library/Simps_Case_Conv.thy"} converts a single equation with
   5.131 +\<^file>\<open>~~/src/HOL/Library/Simps_Case_Conv.thy\<close> converts a single equation with
   5.132  a complex case expression on the right-hand side into a set of pattern-matching
   5.133  equations. For example,
   5.134  \<close>
   5.135 @@ -3249,7 +3249,7 @@
   5.136  
   5.137  \noindent
   5.138  The \keyw{case_of_simps} command provided by theory
   5.139 -@{file "~~/src/HOL/Library/Simps_Case_Conv.thy"} converts a set of
   5.140 +\<^file>\<open>~~/src/HOL/Library/Simps_Case_Conv.thy\<close> converts a set of
   5.141  pattern-matching equations into single equation with a complex case expression
   5.142  on the right-hand side (cf.\ @{command simps_of_case}). For example,
   5.143  \<close>
   5.144 @@ -3386,7 +3386,7 @@
   5.145  @{text "('a\<^sub>1 \<Rightarrow> nat) \<Rightarrow> \<dots> \<Rightarrow> ('a\<^sub>m \<Rightarrow> nat) \<Rightarrow> u \<Rightarrow> nat"} using
   5.146  the ML function @{ML BNF_LFP_Size.register_size} or
   5.147  @{ML BNF_LFP_Size.register_size_global}. See theory
   5.148 -@{file "~~/src/HOL/Library/Multiset.thy"} for an example.
   5.149 +\<^file>\<open>~~/src/HOL/Library/Multiset.thy\<close> for an example.
   5.150  \<close>
   5.151  
   5.152  
     6.1 --- a/src/Doc/Implementation/Eq.thy	Fri Aug 12 17:49:02 2016 +0200
     6.2 +++ b/src/Doc/Implementation/Eq.thy	Fri Aug 12 17:53:55 2016 +0200
     6.3 @@ -64,10 +64,10 @@
     6.4    @{index_ML Thm.equal_elim: "thm -> thm -> thm"} \\
     6.5    \end{mldecls}
     6.6  
     6.7 -  See also @{file "~~/src/Pure/thm.ML" } for further description of these
     6.8 -  inference rules, and a few more for primitive \<open>\<beta>\<close> and \<open>\<eta>\<close> conversions. Note
     6.9 -  that \<open>\<alpha>\<close> conversion is implicit due to the representation of terms with
    6.10 -  de-Bruijn indices (\secref{sec:terms}).
    6.11 +  See also \<^file>\<open>~~/src/Pure/thm.ML\<close> for further description of these inference
    6.12 +  rules, and a few more for primitive \<open>\<beta>\<close> and \<open>\<eta>\<close> conversions. Note that \<open>\<alpha>\<close>
    6.13 +  conversion is implicit due to the representation of terms with de-Bruijn
    6.14 +  indices (\secref{sec:terms}).
    6.15  \<close>
    6.16  
    6.17  
     7.1 --- a/src/Doc/Implementation/Integration.thy	Fri Aug 12 17:49:02 2016 +0200
     7.2 +++ b/src/Doc/Implementation/Integration.thy	Fri Aug 12 17:53:55 2016 +0200
     7.3 @@ -132,9 +132,9 @@
     7.4  \<close>
     7.5  
     7.6  text %mlex \<open>
     7.7 -  The file @{file "~~/src/HOL/ex/Commands.thy"} shows some example Isar
     7.8 -  command definitions, with the all-important theory header declarations for
     7.9 -  outer syntax keywords.
    7.10 +  The file \<^file>\<open>~~/src/HOL/ex/Commands.thy\<close> shows some example Isar command
    7.11 +  definitions, with the all-important theory header declarations for outer
    7.12 +  syntax keywords.
    7.13  \<close>
    7.14  
    7.15  
     8.1 --- a/src/Doc/Implementation/Logic.thy	Fri Aug 12 17:49:02 2016 +0200
     8.2 +++ b/src/Doc/Implementation/Logic.thy	Fri Aug 12 17:53:55 2016 +0200
     8.3 @@ -1248,11 +1248,11 @@
     8.4  \<close>
     8.5  
     8.6  text %mlex \<open>
     8.7 -  \<^item> @{file "~~/src/HOL/Proofs/ex/Proof_Terms.thy"} provides basic examples
     8.8 -  involving proof terms.
     8.9 +  \<^item> \<^file>\<open>~~/src/HOL/Proofs/ex/Proof_Terms.thy\<close> provides basic examples involving
    8.10 +  proof terms.
    8.11  
    8.12 -  \<^item> @{file "~~/src/HOL/Proofs/ex/XML_Data.thy"} demonstrates export and import
    8.13 -  of proof terms via XML/ML data representation.
    8.14 +  \<^item> \<^file>\<open>~~/src/HOL/Proofs/ex/XML_Data.thy\<close> demonstrates export and import of
    8.15 +  proof terms via XML/ML data representation.
    8.16  \<close>
    8.17  
    8.18  end
     9.1 --- a/src/Doc/Implementation/ML.thy	Fri Aug 12 17:49:02 2016 +0200
     9.2 +++ b/src/Doc/Implementation/ML.thy	Fri Aug 12 17:53:55 2016 +0200
     9.3 @@ -22,8 +22,8 @@
     9.4    The main aspects of Isabelle/ML are introduced below. These first-hand
     9.5    explanations should help to understand how proper Isabelle/ML is to be read
     9.6    and written, and to get access to the wealth of experience that is expressed
     9.7 -  in the source text and its history of changes.\<^footnote>\<open>See @{url
     9.8 -  "http://isabelle.in.tum.de/repos/isabelle"} for the full Mercurial history.
     9.9 +  in the source text and its history of changes.\<^footnote>\<open>See
    9.10 +  \<^url>\<open>http://isabelle.in.tum.de/repos/isabelle\<close> for the full Mercurial history.
    9.11    There are symbolic tags to refer to official Isabelle releases, as opposed
    9.12    to arbitrary \<^emph>\<open>tip\<close> versions that merely reflect snapshots that are never
    9.13    really up-to-date.\<close>
    9.14 @@ -38,9 +38,8 @@
    9.15    really going on and how things really work. This is a non-trivial aim, but
    9.16    it is supported by a certain style of writing Isabelle/ML that has emerged
    9.17    from long years of system development.\<^footnote>\<open>See also the interesting style guide
    9.18 -  for OCaml @{url
    9.19 -  "http://caml.inria.fr/resources/doc/guides/guidelines.en.html"} which shares
    9.20 -  many of our means and ends.\<close>
    9.21 +  for OCaml \<^url>\<open>http://caml.inria.fr/resources/doc/guides/guidelines.en.html\<close>
    9.22 +  which shares many of our means and ends.\<close>
    9.23  
    9.24    The main principle behind any coding style is \<^emph>\<open>consistency\<close>. For a single
    9.25    author of a small program this merely means ``choose your style and stick to
    9.26 @@ -63,8 +62,8 @@
    9.27  text \<open>
    9.28    Isabelle source files have a certain standardized header format (with
    9.29    precise spacing) that follows ancient traditions reaching back to the
    9.30 -  earliest versions of the system by Larry Paulson. See @{file
    9.31 -  "~~/src/Pure/thm.ML"}, for example.
    9.32 +  earliest versions of the system by Larry Paulson. See
    9.33 +  \<^file>\<open>~~/src/Pure/thm.ML\<close>, for example.
    9.34  
    9.35    The header includes at least \<^verbatim>\<open>Title\<close> and \<^verbatim>\<open>Author\<close> entries, followed by a
    9.36    prose description of the purpose of the module. The latter can range from a
    9.37 @@ -1385,8 +1384,8 @@
    9.38    32-bit Poly/ML, and much higher for 64-bit systems.\<close>
    9.39  
    9.40    Structure @{ML_structure IntInf} of SML97 is obsolete and superseded by
    9.41 -  @{ML_structure Int}. Structure @{ML_structure Integer} in @{file
    9.42 -  "~~/src/Pure/General/integer.ML"} provides some additional operations.
    9.43 +  @{ML_structure Int}. Structure @{ML_structure Integer} in
    9.44 +  \<^file>\<open>~~/src/Pure/General/integer.ML\<close> provides some additional operations.
    9.45  \<close>
    9.46  
    9.47  
    9.48 @@ -1445,8 +1444,7 @@
    9.49  text \<open>
    9.50    Apart from @{ML Option.map} most other operations defined in structure
    9.51    @{ML_structure Option} are alien to Isabelle/ML and never used. The
    9.52 -  operations shown above are defined in @{file
    9.53 -  "~~/src/Pure/General/basics.ML"}.
    9.54 +  operations shown above are defined in \<^file>\<open>~~/src/Pure/General/basics.ML\<close>.
    9.55  \<close>
    9.56  
    9.57  
    9.58 @@ -1474,9 +1472,9 @@
    9.59    is required.
    9.60  
    9.61    \<^descr> @{ML member}, @{ML insert}, @{ML remove}, @{ML update} treat lists as a
    9.62 -  set-like container that maintains the order of elements. See @{file
    9.63 -  "~~/src/Pure/library.ML"} for the full specifications (written in ML). There
    9.64 -  are some further derived operations like @{ML union} or @{ML inter}.
    9.65 +  set-like container that maintains the order of elements. See
    9.66 +  \<^file>\<open>~~/src/Pure/library.ML\<close> for the full specifications (written in ML).
    9.67 +  There are some further derived operations like @{ML union} or @{ML inter}.
    9.68  
    9.69    Note that @{ML insert} is conservative about elements that are already a
    9.70    @{ML member} of the list, while @{ML update} ensures that the latest entry
    9.71 @@ -1518,8 +1516,8 @@
    9.72    fold_rev} attempts to preserve the order of elements in the result.
    9.73  
    9.74    This way of merging lists is typical for context data
    9.75 -  (\secref{sec:context-data}). See also @{ML merge} as defined in @{file
    9.76 -  "~~/src/Pure/library.ML"}.
    9.77 +  (\secref{sec:context-data}). See also @{ML merge} as defined in
    9.78 +  \<^file>\<open>~~/src/Pure/library.ML\<close>.
    9.79  \<close>
    9.80  
    9.81  
    9.82 @@ -1555,8 +1553,8 @@
    9.83  
    9.84    Association lists are adequate as simple implementation of finite mappings
    9.85    in many practical situations. A more advanced table structure is defined in
    9.86 -  @{file "~~/src/Pure/General/table.ML"}; that version scales easily to
    9.87 -  thousands or millions of elements.
    9.88 +  \<^file>\<open>~~/src/Pure/General/table.ML\<close>; that version scales easily to thousands or
    9.89 +  millions of elements.
    9.90  \<close>
    9.91  
    9.92  
    9.93 @@ -1782,8 +1780,7 @@
    9.94      on the associated condition variable, and returns the result \<open>y\<close>.
    9.95  
    9.96    There are some further variants of the @{ML Synchronized.guarded_access}
    9.97 -  combinator, see @{file "~~/src/Pure/Concurrent/synchronized.ML"} for
    9.98 -  details.
    9.99 +  combinator, see \<^file>\<open>~~/src/Pure/Concurrent/synchronized.ML\<close> for details.
   9.100  \<close>
   9.101  
   9.102  text %mlex \<open>
   9.103 @@ -1809,8 +1806,8 @@
   9.104  
   9.105  text \<open>
   9.106    \<^medskip>
   9.107 -  See @{file "~~/src/Pure/Concurrent/mailbox.ML"} how to implement a mailbox
   9.108 -  as synchronized variable over a purely functional list.
   9.109 +  See \<^file>\<open>~~/src/Pure/Concurrent/mailbox.ML\<close> how to implement a mailbox as
   9.110 +  synchronized variable over a purely functional list.
   9.111  \<close>
   9.112  
   9.113  
    10.1 --- a/src/Doc/Implementation/Tactic.thy	Fri Aug 12 17:49:02 2016 +0200
    10.2 +++ b/src/Doc/Implementation/Tactic.thy	Fri Aug 12 17:53:55 2016 +0200
    10.3 @@ -168,9 +168,8 @@
    10.4    \end{mldecls}
    10.5  
    10.6    \<^descr> Type @{ML_type tactic} represents tactics. The well-formedness conditions
    10.7 -  described above need to be observed. See also @{file
    10.8 -  "~~/src/Pure/General/seq.ML"} for the underlying implementation of lazy
    10.9 -  sequences.
   10.10 +  described above need to be observed. See also \<^file>\<open>~~/src/Pure/General/seq.ML\<close>
   10.11 +  for the underlying implementation of lazy sequences.
   10.12  
   10.13    \<^descr> Type @{ML_type "int -> tactic"} represents tactics with explicit subgoal
   10.14    addressing, with well-formedness conditions as described above.
    11.1 --- a/src/Doc/Isar_Ref/Document_Preparation.thy	Fri Aug 12 17:49:02 2016 +0200
    11.2 +++ b/src/Doc/Isar_Ref/Document_Preparation.thy	Fri Aug 12 17:53:55 2016 +0200
    11.3 @@ -40,7 +40,7 @@
    11.4    Markup commands provide a structured way to insert text into the document
    11.5    generated from a theory. Each markup command takes a single @{syntax text}
    11.6    argument, which is passed as argument to a corresponding {\LaTeX} macro. The
    11.7 -  default macros provided by @{file "~~/lib/texinputs/isabelle.sty"} can be
    11.8 +  default macros provided by \<^file>\<open>~~/lib/texinputs/isabelle.sty\<close> can be
    11.9    redefined according to the needs of the underlying document and {\LaTeX}
   11.10    styles.
   11.11  
   11.12 @@ -420,8 +420,8 @@
   11.13    text_raw} (\secref{sec:markup}) consist of plain text. Its internal
   11.14    structure consists of paragraphs and (nested) lists, using special Isabelle
   11.15    symbols and some rules for indentation and blank lines. This quasi-visual
   11.16 -  format resembles \<^emph>\<open>Markdown\<close>\<^footnote>\<open>@{url "http://commonmark.org"}\<close>, but the
   11.17 -  full complexity of that notation is avoided.
   11.18 +  format resembles \<^emph>\<open>Markdown\<close>\<^footnote>\<open>\<^url>\<open>http://commonmark.org\<close>\<close>, but the full
   11.19 +  complexity of that notation is avoided.
   11.20  
   11.21    This is a summary of the main principles of minimal Markdown in Isabelle:
   11.22  
   11.23 @@ -495,8 +495,8 @@
   11.24  
   11.25    \<^medskip>
   11.26    Command tags merely produce certain markup environments for type-setting.
   11.27 -  The meaning of these is determined by {\LaTeX} macros, as defined in @{file
   11.28 -  "~~/lib/texinputs/isabelle.sty"} or by the document author. The Isabelle
   11.29 +  The meaning of these is determined by {\LaTeX} macros, as defined in
   11.30 +  \<^file>\<open>~~/lib/texinputs/isabelle.sty\<close> or by the document author. The Isabelle
   11.31    document preparation tools also provide some high-level options to specify
   11.32    the meaning of arbitrary tags to ``keep'', ``drop'', or ``fold'' the
   11.33    corresponding parts of the text. Logic sessions may also specify ``document
   11.34 @@ -517,8 +517,8 @@
   11.35    \<close>}
   11.36  
   11.37    The @{antiquotation rail} antiquotation allows to include syntax diagrams
   11.38 -  into Isabelle documents. {\LaTeX} requires the style file @{file
   11.39 -  "~~/lib/texinputs/railsetup.sty"}, which can be used via
   11.40 +  into Isabelle documents. {\LaTeX} requires the style file
   11.41 +  \<^file>\<open>~~/lib/texinputs/railsetup.sty\<close>, which can be used via
   11.42    \<^verbatim>\<open>\usepackage{railsetup}\<close> in \<^verbatim>\<open>root.tex\<close>, for example.
   11.43  
   11.44    The rail specification language is quoted here as Isabelle @{syntax string}
    12.1 --- a/src/Doc/Isar_Ref/Framework.thy	Fri Aug 12 17:49:02 2016 +0200
    12.2 +++ b/src/Doc/Isar_Ref/Framework.thy	Fri Aug 12 17:53:55 2016 +0200
    12.3 @@ -89,13 +89,13 @@
    12.4    \<^medskip>
    12.5    Concrete applications require another intermediate layer: an object-logic.
    12.6    Isabelle/HOL @{cite "isa-tutorial"} (simply-typed set-theory) is most
    12.7 -  commonly used; elementary examples are given in the directory @{dir
    12.8 -  "~~/src/HOL/Isar_Examples"}. Some examples demonstrate how to start a fresh
    12.9 +  commonly used; elementary examples are given in the directory
   12.10 +  \<^dir>\<open>~~/src/HOL/Isar_Examples\<close>. Some examples demonstrate how to start a fresh
   12.11    object-logic from Isabelle/Pure, and use Isar proofs from the very start,
   12.12    despite the lack of advanced proof tools at such an early stage (e.g.\ see
   12.13 -  @{file "~~/src/HOL/Isar_Examples/Higher_Order_Logic.thy"}). Isabelle/FOL
   12.14 -  @{cite "isabelle-logics"} and Isabelle/ZF @{cite "isabelle-ZF"} also work,
   12.15 -  but are much less developed.
   12.16 +  \<^file>\<open>~~/src/HOL/Isar_Examples/Higher_Order_Logic.thy\<close>). Isabelle/FOL @{cite
   12.17 +  "isabelle-logics"} and Isabelle/ZF @{cite "isabelle-ZF"} also work, but are
   12.18 +  much less developed.
   12.19  
   12.20    In order to illustrate natural deduction in Isar, we shall subsequently
   12.21    refer to the background theory and library of Isabelle/HOL. This includes
   12.22 @@ -524,7 +524,7 @@
   12.23    may be populated later. The command \<^theory_text>\<open>method_setup\<close> allows to define proof
   12.24    methods semantically in Isabelle/ML. The Eisbach language allows to define
   12.25    proof methods symbolically, as recursive expressions over existing methods
   12.26 -  @{cite "Matichuk-et-al:2014"}; see also @{dir "~~/src/HOL/Eisbach"}.
   12.27 +  @{cite "Matichuk-et-al:2014"}; see also \<^dir>\<open>~~/src/HOL/Eisbach\<close>.
   12.28  
   12.29    Methods use the facts indicated by \<^theory_text>\<open>then\<close> or \<^theory_text>\<open>using\<close>, and then operate on
   12.30    the goal state. Some basic methods are predefined in Pure: ``@{method "-"}''
    13.1 --- a/src/Doc/Isar_Ref/HOL_Specific.thy	Fri Aug 12 17:49:02 2016 +0200
    13.2 +++ b/src/Doc/Isar_Ref/HOL_Specific.thy	Fri Aug 12 17:53:55 2016 +0200
    13.3 @@ -538,8 +538,8 @@
    13.4    \<^descr> @{method (HOL) induction_schema} derives user-specified induction rules
    13.5    from well-founded induction and completeness of patterns. This factors out
    13.6    some operations that are done internally by the function package and makes
    13.7 -  them available separately. See @{file "~~/src/HOL/ex/Induction_Schema.thy"}
    13.8 -  for examples.
    13.9 +  them available separately. See \<^file>\<open>~~/src/HOL/ex/Induction_Schema.thy\<close> for
   13.10 +  examples.
   13.11  \<close>
   13.12  
   13.13  
   13.14 @@ -659,8 +659,8 @@
   13.15    Adhoc overloading allows to overload a constant depending on its type.
   13.16    Typically this involves the introduction of an uninterpreted constant (used
   13.17    for input and output) and the addition of some variants (used internally).
   13.18 -  For examples see @{file "~~/src/HOL/ex/Adhoc_Overloading_Examples.thy"} and
   13.19 -  @{file "~~/src/HOL/Library/Monad_Syntax.thy"}.
   13.20 +  For examples see \<^file>\<open>~~/src/HOL/ex/Adhoc_Overloading_Examples.thy\<close> and
   13.21 +  \<^file>\<open>~~/src/HOL/Library/Monad_Syntax.thy\<close>.
   13.22  
   13.23    @{rail \<open>
   13.24      (@@{command adhoc_overloading} | @@{command no_adhoc_overloading})
   13.25 @@ -1013,7 +1013,7 @@
   13.26  
   13.27  subsubsection \<open>Examples\<close>
   13.28  
   13.29 -text \<open>See @{file "~~/src/HOL/ex/Records.thy"}, for example.\<close>
   13.30 +text \<open>See \<^file>\<open>~~/src/HOL/ex/Records.thy\<close>, for example.\<close>
   13.31  
   13.32  
   13.33  section \<open>Semantic subtype definitions \label{sec:hol-typedef}\<close>
   13.34 @@ -1411,28 +1411,26 @@
   13.35    \<^descr> @{attribute (HOL) quot_map} registers a quotient map theorem, a theorem
   13.36    showing how to ``lift'' quotients over type constructors. E.g.\ @{term
   13.37    "Quotient R Abs Rep T \<Longrightarrow> Quotient (rel_set R) (image Abs) (image Rep)
   13.38 -  (rel_set T)"}. For examples see @{file "~~/src/HOL/Lifting_Set.thy"} or
   13.39 -  @{file "~~/src/HOL/Lifting.thy"}. This property is proved automatically if
   13.40 -  the involved type is BNF without dead variables.
   13.41 +  (rel_set T)"}. For examples see \<^file>\<open>~~/src/HOL/Lifting_Set.thy\<close> or
   13.42 +  \<^file>\<open>~~/src/HOL/Lifting.thy\<close>. This property is proved automatically if the
   13.43 +  involved type is BNF without dead variables.
   13.44  
   13.45    \<^descr> @{attribute (HOL) relator_eq_onp} registers a theorem that shows that a
   13.46    relator applied to an equality restricted by a predicate @{term P} (i.e.\
   13.47    @{term "eq_onp P"}) is equal to a predicator applied to the @{term P}. The
   13.48    combinator @{const eq_onp} is used for internal encoding of proper subtypes.
   13.49    Such theorems allows the package to hide \<open>eq_onp\<close> from a user in a
   13.50 -  user-readable form of a respectfulness theorem. For examples see @{file
   13.51 -  "~~/src/HOL/Lifting_Set.thy"} or @{file "~~/src/HOL/Lifting.thy"}. This
   13.52 -  property is proved automatically if the involved type is BNF without dead
   13.53 -  variables.
   13.54 +  user-readable form of a respectfulness theorem. For examples see
   13.55 +  \<^file>\<open>~~/src/HOL/Lifting_Set.thy\<close> or \<^file>\<open>~~/src/HOL/Lifting.thy\<close>. This property
   13.56 +  is proved automatically if the involved type is BNF without dead variables.
   13.57  
   13.58    \<^descr> @{attribute (HOL) "relator_mono"} registers a property describing a
   13.59    monotonicity of a relator. E.g.\ @{prop "A \<le> B \<Longrightarrow> rel_set A \<le> rel_set B"}.
   13.60    This property is needed for proving a stronger transfer rule in
   13.61    @{command_def (HOL) "lift_definition"} when a parametricity theorem for the
   13.62    raw term is specified and also for the reflexivity prover. For examples see
   13.63 -  @{file "~~/src/HOL/Lifting_Set.thy"} or @{file "~~/src/HOL/Lifting.thy"}.
   13.64 -  This property is proved automatically if the involved type is BNF without
   13.65 -  dead variables.
   13.66 +  \<^file>\<open>~~/src/HOL/Lifting_Set.thy\<close> or \<^file>\<open>~~/src/HOL/Lifting.thy\<close>. This property
   13.67 +  is proved automatically if the involved type is BNF without dead variables.
   13.68  
   13.69    \<^descr> @{attribute (HOL) "relator_distr"} registers a property describing a
   13.70    distributivity of the relation composition and a relator. E.g.\ \<open>rel_set R
   13.71 @@ -1443,9 +1441,9 @@
   13.72    specified each direction separately and also register multiple theorems with
   13.73    different set of assumptions. This attribute can be used only after the
   13.74    monotonicity property was already registered by @{attribute (HOL)
   13.75 -  "relator_mono"}. For examples see @{file "~~/src/HOL/Lifting_Set.thy"} or
   13.76 -  @{file "~~/src/HOL/Lifting.thy"}. This property is proved automatically if
   13.77 -  the involved type is BNF without dead variables.
   13.78 +  "relator_mono"}. For examples see \<^file>\<open>~~/src/HOL/Lifting_Set.thy\<close> or
   13.79 +  \<^file>\<open>~~/src/HOL/Lifting.thy\<close>. This property is proved automatically if the
   13.80 +  involved type is BNF without dead variables.
   13.81  
   13.82    \<^descr> @{attribute (HOL) quot_del} deletes a corresponding Quotient theorem from
   13.83    the Lifting infrastructure and thus de-register the corresponding quotient.
   13.84 @@ -1524,7 +1522,7 @@
   13.85    "transfer_step"}+, @{method (HOL) "transfer_end"}) and @{method (HOL)
   13.86    "transfer_prover"} = (@{method (HOL) "transfer_prover_start"}, @{method
   13.87    (HOL) "transfer_step"}+, @{method (HOL) "transfer_prover_end"}). For usage
   13.88 -  examples see @{file "~~/src/HOL/ex/Transfer_Debug.thy"}
   13.89 +  examples see \<^file>\<open>~~/src/HOL/ex/Transfer_Debug.thy\<close>.
   13.90  
   13.91    \<^descr> @{attribute (HOL) "untransferred"} proves the same equivalent theorem as
   13.92    @{method (HOL) "transfer"} internally does.
   13.93 @@ -1566,17 +1564,15 @@
   13.94    relators of various type constructors, e.g. @{term "rel_set (op =) = (op
   13.95    =)"}. The @{method (HOL) transfer} method uses these lemmas to infer
   13.96    transfer rules for non-polymorphic constants on the fly. For examples see
   13.97 -  @{file "~~/src/HOL/Lifting_Set.thy"} or @{file "~~/src/HOL/Lifting.thy"}.
   13.98 -  This property is proved automatically if the involved type is BNF without
   13.99 -  dead variables.
  13.100 +  \<^file>\<open>~~/src/HOL/Lifting_Set.thy\<close> or \<^file>\<open>~~/src/HOL/Lifting.thy\<close>. This property
  13.101 +  is proved automatically if the involved type is BNF without dead variables.
  13.102  
  13.103    \<^descr> @{attribute_def (HOL) "relator_domain"} attribute collects rules
  13.104    describing domains of relators by predicators. E.g.\ @{term "Domainp
  13.105    (rel_set T) = (\<lambda>A. Ball A (Domainp T))"}. This allows the package to lift
  13.106 -  transfer domain rules through type constructors. For examples see @{file
  13.107 -  "~~/src/HOL/Lifting_Set.thy"} or @{file "~~/src/HOL/Lifting.thy"}. This
  13.108 -  property is proved automatically if the involved type is BNF without dead
  13.109 -  variables.
  13.110 +  transfer domain rules through type constructors. For examples see
  13.111 +  \<^file>\<open>~~/src/HOL/Lifting_Set.thy\<close> or \<^file>\<open>~~/src/HOL/Lifting.thy\<close>. This property
  13.112 +  is proved automatically if the involved type is BNF without dead variables.
  13.113  
  13.114  
  13.115    Theoretical background can be found in @{cite
  13.116 @@ -2082,14 +2078,13 @@
  13.117    \<close>}
  13.118  
  13.119    \<^descr> @{method (HOL) meson} implements Loveland's model elimination procedure
  13.120 -  @{cite "loveland-78"}. See @{file "~~/src/HOL/ex/Meson_Test.thy"} for
  13.121 -  examples.
  13.122 +  @{cite "loveland-78"}. See \<^file>\<open>~~/src/HOL/ex/Meson_Test.thy\<close> for examples.
  13.123  
  13.124    \<^descr> @{method (HOL) metis} combines ordered resolution and ordered
  13.125    paramodulation to find first-order (or mildly higher-order) proofs. The
  13.126    first optional argument specifies a type encoding; see the Sledgehammer
  13.127 -  manual @{cite "isabelle-sledgehammer"} for details. The directory @{dir
  13.128 -  "~~/src/HOL/Metis_Examples"} contains several small theories developed to a
  13.129 +  manual @{cite "isabelle-sledgehammer"} for details. The directory
  13.130 +  \<^dir>\<open>~~/src/HOL/Metis_Examples\<close> contains several small theories developed to a
  13.131    large extent using @{method (HOL) metis}.
  13.132  \<close>
  13.133  
  13.134 @@ -2168,7 +2163,7 @@
  13.135  (*<*)end(*>*)
  13.136  
  13.137  text \<open>
  13.138 - See also @{file "~~/src/HOL/ex/Groebner_Examples.thy"}.
  13.139 +  See also \<^file>\<open>~~/src/HOL/ex/Groebner_Examples.thy\<close>.
  13.140  \<close>
  13.141  
  13.142  
  13.143 @@ -2185,8 +2180,8 @@
  13.144  
  13.145    \<^descr> @{method (HOL) coherent} solves problems of \<^emph>\<open>Coherent Logic\<close> @{cite
  13.146    "Bezem-Coquand:2005"}, which covers applications in confluence theory,
  13.147 -  lattice theory and projective geometry. See @{file
  13.148 -  "~~/src/HOL/ex/Coherent.thy"} for some examples.
  13.149 +  lattice theory and projective geometry. See \<^file>\<open>~~/src/HOL/ex/Coherent.thy\<close>
  13.150 +  for some examples.
  13.151  \<close>
  13.152  
  13.153  
    14.1 --- a/src/Doc/Isar_Ref/Inner_Syntax.thy	Fri Aug 12 17:49:02 2016 +0200
    14.2 +++ b/src/Doc/Isar_Ref/Inner_Syntax.thy	Fri Aug 12 17:53:55 2016 +0200
    14.3 @@ -571,8 +571,8 @@
    14.4    float_token}, @{syntax (inner) str_token}, @{syntax (inner) string_token},
    14.5    and @{syntax (inner) cartouche} are not used in Pure. Object-logics may
    14.6    implement numerals and string literals by adding appropriate syntax
    14.7 -  declarations, together with some translation functions (e.g.\ see @{file
    14.8 -  "~~/src/HOL/Tools/string_syntax.ML"}).
    14.9 +  declarations, together with some translation functions (e.g.\ see
   14.10 +  \<^file>\<open>~~/src/HOL/Tools/string_syntax.ML\<close>).
   14.11  
   14.12    The derived categories @{syntax_def (inner) num_const}, and @{syntax_def
   14.13    (inner) float_const}, provide robust access to the respective tokens: the
    15.1 --- a/src/Doc/Isar_Ref/Spec.thy	Fri Aug 12 17:49:02 2016 +0200
    15.2 +++ b/src/Doc/Isar_Ref/Spec.thy	Fri Aug 12 17:53:55 2016 +0200
    15.3 @@ -1303,8 +1303,8 @@
    15.4    the scope of the resulting theory.
    15.5  
    15.6  
    15.7 -  See @{file "~~/src/HOL/ex/Iff_Oracle.thy"} for a worked example of defining
    15.8 -  a new primitive rule as oracle, and turning it into a proof method.
    15.9 +  See \<^file>\<open>~~/src/HOL/ex/Iff_Oracle.thy\<close> for a worked example of defining a new
   15.10 +  primitive rule as oracle, and turning it into a proof method.
   15.11  \<close>
   15.12  
   15.13  
    16.1 --- a/src/Doc/Isar_Ref/Synopsis.thy	Fri Aug 12 17:49:02 2016 +0200
    16.2 +++ b/src/Doc/Isar_Ref/Synopsis.thy	Fri Aug 12 17:53:55 2016 +0200
    16.3 @@ -214,7 +214,7 @@
    16.4  section \<open>Calculational reasoning \label{sec:calculations-synopsis}\<close>
    16.5  
    16.6  text \<open>
    16.7 -  For example, see @{file "~~/src/HOL/Isar_Examples/Group.thy"}.
    16.8 +  For example, see \<^file>\<open>~~/src/HOL/Isar_Examples/Group.thy\<close>.
    16.9  \<close>
   16.10  
   16.11  
    17.1 --- a/src/Doc/JEdit/JEdit.thy	Fri Aug 12 17:49:02 2016 +0200
    17.2 +++ b/src/Doc/JEdit/JEdit.thy	Fri Aug 12 17:53:55 2016 +0200
    17.3 @@ -37,11 +37,10 @@
    17.4      given up; instead there is direct support for editing of source text, with
    17.5      rich formal markup for GUI rendering.
    17.6  
    17.7 -    \<^descr>[jEdit] is a sophisticated text editor\<^footnote>\<open>@{url "http://www.jedit.org"}\<close>
    17.8 -    implemented in Java\<^footnote>\<open>@{url "http://www.java.com"}\<close>. It is easily
    17.9 -    extensible by plugins written in any language that works on the JVM. In
   17.10 -    the context of Isabelle this is always Scala\<^footnote>\<open>@{url
   17.11 -    "http://www.scala-lang.org"}\<close>.
   17.12 +    \<^descr>[jEdit] is a sophisticated text editor\<^footnote>\<open>\<^url>\<open>http://www.jedit.org\<close>\<close>
   17.13 +    implemented in Java\<^footnote>\<open>\<^url>\<open>http://www.java.com\<close>\<close>. It is easily extensible by
   17.14 +    plugins written in any language that works on the JVM. In the context of
   17.15 +    Isabelle this is always Scala\<^footnote>\<open>\<^url>\<open>http://www.scala-lang.org\<close>\<close>.
   17.16  
   17.17      \<^descr>[Isabelle/jEdit] is the main application of the PIDE framework and the
   17.18      default user-interface for Isabelle. It targets both beginners and
   17.19 @@ -214,7 +213,7 @@
   17.20    additional keyboard shortcuts for Isabelle-specific functionality. Users may
   17.21    change their keymap later, but need to copy some keyboard shortcuts manually
   17.22    (see also @{path "$ISABELLE_HOME_USER/jedit/keymaps"} versus \<^verbatim>\<open>shortcut\<close>
   17.23 -  properties in @{file "$ISABELLE_HOME/src/Tools/jEdit/src/jEdit.props"}).
   17.24 +  properties in \<^file>\<open>$ISABELLE_HOME/src/Tools/jEdit/src/jEdit.props\<close>).
   17.25  \<close>
   17.26  
   17.27  
   17.28 @@ -271,8 +270,8 @@
   17.29  
   17.30    The \<^verbatim>\<open>-b\<close> and \<^verbatim>\<open>-f\<close> options control the self-build mechanism of
   17.31    Isabelle/jEdit. This is only relevant for building from sources, which also
   17.32 -  requires an auxiliary \<^verbatim>\<open>jedit_build\<close> component from @{url
   17.33 -  "http://isabelle.in.tum.de/components"}. The official Isabelle release
   17.34 +  requires an auxiliary \<^verbatim>\<open>jedit_build\<close> component from
   17.35 +  \<^url>\<open>http://isabelle.in.tum.de/components\<close>. The official Isabelle release
   17.36    already includes a pre-built version of Isabelle/jEdit.
   17.37  
   17.38    \<^bigskip>
   17.39 @@ -468,8 +467,8 @@
   17.40    ``\<^verbatim>\<open>\<alpha>\<close>''. For the editor front-end, a certain subset of symbols is rendered
   17.41    physically via Unicode glyphs, in order to show ``\<^verbatim>\<open>\<alpha>\<close>'' as ``\<open>\<alpha>\<close>'', for
   17.42    example. This symbol interpretation is specified by the Isabelle system
   17.43 -  distribution in @{file "$ISABELLE_HOME/etc/symbols"} and may be augmented by
   17.44 -  the user in @{path "$ISABELLE_HOME_USER/etc/symbols"}.
   17.45 +  distribution in \<^file>\<open>$ISABELLE_HOME/etc/symbols\<close> and may be augmented by the
   17.46 +  user in @{path "$ISABELLE_HOME_USER/etc/symbols"}.
   17.47  
   17.48    The appendix of @{cite "isabelle-isar-ref"} gives an overview of the
   17.49    standard interpretation of finitely many symbols from the infinite
   17.50 @@ -550,7 +549,7 @@
   17.51    \<^verbatim>\<open>\lambda\<close>, or its ASCII abbreviation \<^verbatim>\<open>%\<close> by the Unicode rendering.
   17.52  
   17.53    The following table is an extract of the information provided by the
   17.54 -  standard @{file "$ISABELLE_HOME/etc/symbols"} file:
   17.55 +  standard \<^file>\<open>$ISABELLE_HOME/etc/symbols\<close> file:
   17.56  
   17.57    \<^medskip>
   17.58    \begin{tabular}{lll}
   17.59 @@ -659,9 +658,8 @@
   17.60    platforms. Isabelle/ML on Windows uses Unix-style path notation, too, and
   17.61    driver letter representation as in Cygwin (e.g.\ \<^verbatim>\<open>/cygdrive/c\<close>). Moreover,
   17.62    environment variables from the Isabelle process may be used freely, e.g.\
   17.63 -  @{file "$ISABELLE_HOME/etc/symbols"} or @{file "$POLYML_HOME/README"}. There
   17.64 -  are special shortcuts: @{dir "~"} for @{dir "$USER_HOME"} and @{dir "~~"}
   17.65 -  for @{dir "$ISABELLE_HOME"}.
   17.66 +  \<^file>\<open>$ISABELLE_HOME/etc/symbols\<close> or \<^file>\<open>$POLYML_HOME/README\<close>. There are special
   17.67 +  shortcuts: \<^dir>\<open>~\<close> for \<^dir>\<open>$USER_HOME\<close> and \<^dir>\<open>~~\<close> for \<^dir>\<open>$ISABELLE_HOME\<close>.
   17.68  
   17.69    \<^medskip>
   17.70    Since jEdit happens to support environment variables within file
   17.71 @@ -848,8 +846,8 @@
   17.72    further tricks to manage markup of ML files, such that Isabelle/HOL may be
   17.73    edited conveniently in the Prover IDE on small machines with only 8\,GB of
   17.74    main memory. Using \<^verbatim>\<open>Pure\<close> as logic session image, the exploration may start
   17.75 -  at the top @{file "$ISABELLE_HOME/src/HOL/Main.thy"} or the bottom @{file
   17.76 -  "$ISABELLE_HOME/src/HOL/HOL.thy"}, for example.
   17.77 +  at the top \<^file>\<open>$ISABELLE_HOME/src/HOL/Main.thy\<close> or the bottom
   17.78 +  \<^file>\<open>$ISABELLE_HOME/src/HOL/HOL.thy\<close>, for example.
   17.79  
   17.80    Initially, before an auxiliary file is opened in the editor, the prover
   17.81    reads its content from the physical file-system. After the file is opened
   17.82 @@ -874,8 +872,8 @@
   17.83  
   17.84    Warnings, errors, and other useful markup is attached directly to the
   17.85    positions in the auxiliary file buffer, in the manner of standard IDEs. By
   17.86 -  using the load command @{command SML_file} as explained in @{file
   17.87 -  "$ISABELLE_HOME/src/Tools/SML/Examples.thy"}, Isabelle/jEdit may be used as
   17.88 +  using the load command @{command SML_file} as explained in
   17.89 +  \<^file>\<open>$ISABELLE_HOME/src/Tools/SML/Examples.thy\<close>, Isabelle/jEdit may be used as
   17.90    fully-featured IDE for Standard ML, independently of theory or proof
   17.91    development: the required theory merely serves as some kind of project file
   17.92    for a collection of SML source modules.
   17.93 @@ -1044,8 +1042,7 @@
   17.94  
   17.95      \<^item> The \<^emph>\<open>Search\<close> field allows to highlight query output according to some
   17.96      regular expression, in the notation that is commonly used on the Java
   17.97 -    platform.\<^footnote>\<open>@{url
   17.98 -    "https://docs.oracle.com/javase/8/docs/api/java/util/regex/Pattern.html"}\<close>
   17.99 +    platform.\<^footnote>\<open>\<^url>\<open>https://docs.oracle.com/javase/8/docs/api/java/util/regex/Pattern.html\<close>\<close>
  17.100      This may serve as an additional visual filter of the result.
  17.101  
  17.102      \<^item> The \<^emph>\<open>Zoom\<close> box controls the font size of the output area.
  17.103 @@ -1240,9 +1237,8 @@
  17.104  
  17.105  text \<open>
  17.106    The completion tables for Isabelle symbols (\secref{sec:symbols}) are
  17.107 -  determined statically from @{file "$ISABELLE_HOME/etc/symbols"} and
  17.108 -  @{path "$ISABELLE_HOME_USER/etc/symbols"} for each symbol
  17.109 -  specification as follows:
  17.110 +  determined statically from \<^file>\<open>$ISABELLE_HOME/etc/symbols\<close> and @{path
  17.111 +  "$ISABELLE_HOME_USER/etc/symbols"} for each symbol specification as follows:
  17.112  
  17.113    \<^medskip>
  17.114    \begin{tabular}{ll}
  17.115 @@ -1272,13 +1268,12 @@
  17.116    which do not allow arbitrary backslash sequences.
  17.117  
  17.118    \<^medskip>
  17.119 -  Additional abbreviations may be specified in @{file
  17.120 -  "$ISABELLE_HOME/etc/abbrevs"} and @{path "$ISABELLE_HOME_USER/etc/abbrevs"}.
  17.121 -  The file content follows general Isar outer syntax @{cite
  17.122 -  "isabelle-isar-ref"}. Abbreviations are specified as
  17.123 -  ``\<open>abbrev\<close>~\<^verbatim>\<open>=\<close>~\<open>text\<close>'' pairs. The replacement \<open>text\<close> may consist of more
  17.124 -  than just one symbol; otherwise the meaning is the same as a symbol
  17.125 -  specification ``\<open>sym\<close>~\<^verbatim>\<open>abbrev:\<close>~\<open>abbrev\<close>'' within @{path
  17.126 +  Additional abbreviations may be specified in \<^file>\<open>$ISABELLE_HOME/etc/abbrevs\<close>
  17.127 +  and @{path "$ISABELLE_HOME_USER/etc/abbrevs"}. The file content follows
  17.128 +  general Isar outer syntax @{cite "isabelle-isar-ref"}. Abbreviations are
  17.129 +  specified as ``\<open>abbrev\<close>~\<^verbatim>\<open>=\<close>~\<open>text\<close>'' pairs. The replacement \<open>text\<close> may
  17.130 +  consist of more than just one symbol; otherwise the meaning is the same as a
  17.131 +  symbol specification ``\<open>sym\<close>~\<^verbatim>\<open>abbrev:\<close>~\<open>abbrev\<close>'' within @{path
  17.132    "etc/symbols"}.
  17.133  \<close>
  17.134  
  17.135 @@ -1718,10 +1713,10 @@
  17.136  
  17.137  text \<open>
  17.138    Document text is internally structured in paragraphs and nested lists, using
  17.139 -  notation that is similar to Markdown\<^footnote>\<open>@{url "http://commonmark.org"}\<close>. There
  17.140 -  are special control symbols for items of different kinds of lists,
  17.141 -  corresponding to \<^verbatim>\<open>itemize\<close>, \<^verbatim>\<open>enumerate\<close>, \<^verbatim>\<open>description\<close> in {\LaTeX}. This
  17.142 -  is illustrated in for \<^verbatim>\<open>itemize\<close> in \figref{fig:markdown-document}.
  17.143 +  notation that is similar to Markdown\<^footnote>\<open>\<^url>\<open>http://commonmark.org\<close>\<close>. There are
  17.144 +  special control symbols for items of different kinds of lists, corresponding
  17.145 +  to \<^verbatim>\<open>itemize\<close>, \<^verbatim>\<open>enumerate\<close>, \<^verbatim>\<open>description\<close> in {\LaTeX}. This is illustrated
  17.146 +  in for \<^verbatim>\<open>itemize\<close> in \figref{fig:markdown-document}.
  17.147  
  17.148    \begin{figure}[!htb]
  17.149    \begin{center}
  17.150 @@ -1781,7 +1776,7 @@
  17.151  chapter \<open>ML debugging within the Prover IDE\<close>
  17.152  
  17.153  text \<open>
  17.154 -  Isabelle/ML is based on Poly/ML\<^footnote>\<open>@{url "http://www.polyml.org"}\<close> and thus
  17.155 +  Isabelle/ML is based on Poly/ML\<^footnote>\<open>\<^url>\<open>http://www.polyml.org\<close>\<close> and thus
  17.156    benefits from the source-level debugger of that implementation of Standard
  17.157    ML. The Prover IDE provides the \<^emph>\<open>Debugger\<close> dockable to connect to running
  17.158    ML threads, inspect the stack frame with local ML bindings, and evaluate ML
    18.1 --- a/src/Doc/Locales/Examples3.thy	Fri Aug 12 17:49:02 2016 +0200
    18.2 +++ b/src/Doc/Locales/Examples3.thy	Fri Aug 12 17:53:55 2016 +0200
    18.3 @@ -525,7 +525,7 @@
    18.4  
    18.5    The sources of this tutorial, which include all proofs, are
    18.6    available with the Isabelle distribution at
    18.7 -  @{url "http://isabelle.in.tum.de"}.
    18.8 +  \<^url>\<open>http://isabelle.in.tum.de\<close>.
    18.9  \<close>
   18.10  
   18.11  text \<open>
    19.1 --- a/src/Doc/Main/Main_Doc.thy	Fri Aug 12 17:49:02 2016 +0200
    19.2 +++ b/src/Doc/Main/Main_Doc.thy	Fri Aug 12 17:53:55 2016 +0200
    19.3 @@ -26,7 +26,7 @@
    19.4  text\<open>
    19.5  
    19.6  \begin{abstract}
    19.7 -This document lists the main types, functions and syntax provided by theory @{theory Main}. It is meant as a quick overview of what is available. For infix operators and their precedences see the final section. The sophisticated class structure is only hinted at. For details see @{url "http://isabelle.in.tum.de/library/HOL/"}.
    19.8 +This document lists the main types, functions and syntax provided by theory @{theory Main}. It is meant as a quick overview of what is available. For infix operators and their precedences see the final section. The sophisticated class structure is only hinted at. For details see \<^url>\<open>http://isabelle.in.tum.de/library/HOL\<close>.
    19.9  \end{abstract}
   19.10  
   19.11  \section*{HOL}
    20.1 --- a/src/Doc/Prog_Prove/Basics.thy	Fri Aug 12 17:49:02 2016 +0200
    20.2 +++ b/src/Doc/Prog_Prove/Basics.thy	Fri Aug 12 17:53:55 2016 +0200
    20.3 @@ -124,9 +124,9 @@
    20.4  \end{warn}
    20.5  
    20.6  In addition to the theories that come with the Isabelle/HOL distribution
    20.7 -(see @{url "http://isabelle.in.tum.de/library/HOL/"})
    20.8 +(see \<^url>\<open>http://isabelle.in.tum.de/library/HOL\<close>)
    20.9  there is also the \emph{Archive of Formal Proofs}
   20.10 -at @{url "http://afp.sourceforge.net"}, a growing collection of Isabelle theories
   20.11 +at \<^url>\<open>http://afp.sourceforge.net\<close>, a growing collection of Isabelle theories
   20.12  that everybody can contribute to.
   20.13  
   20.14  \subsection{Quotation Marks}
    21.1 --- a/src/Doc/System/Environment.thy	Fri Aug 12 17:49:02 2016 +0200
    21.2 +++ b/src/Doc/System/Environment.thy	Fri Aug 12 17:53:55 2016 +0200
    21.3 @@ -44,11 +44,10 @@
    21.4      that the Isabelle executables either have to be run from their original
    21.5      location in the distribution directory, or via the executable objects
    21.6      created by the @{tool install} tool. Symbolic links are admissible, but a
    21.7 -    plain copy of the @{dir "$ISABELLE_HOME/bin"} files will not work!
    21.8 +    plain copy of the \<^dir>\<open>$ISABELLE_HOME/bin\<close> files will not work!
    21.9  
   21.10 -    \<^enum> The file @{file "$ISABELLE_HOME/etc/settings"} is run as a
   21.11 -    @{executable_ref bash} shell script with the auto-export option for
   21.12 -    variables enabled.
   21.13 +    \<^enum> The file \<^file>\<open>$ISABELLE_HOME/etc/settings\<close> is run as a @{executable_ref
   21.14 +    bash} shell script with the auto-export option for variables enabled.
   21.15  
   21.16      This file holds a rather long list of shell variable assignments, thus
   21.17      providing the site-wide default settings. The Isabelle distribution
   21.18 @@ -63,8 +62,8 @@
   21.19  
   21.20      Thus individual users may override the site-wide defaults. Typically, a
   21.21      user settings file contains only a few lines, with some assignments that
   21.22 -    are actually changed. Never copy the central @{file
   21.23 -    "$ISABELLE_HOME/etc/settings"} file!
   21.24 +    are actually changed. Never copy the central
   21.25 +    \<^file>\<open>$ISABELLE_HOME/etc/settings\<close> file!
   21.26  
   21.27    Since settings files are regular GNU @{executable_def bash} scripts, one may
   21.28    use complex shell commands, such as \<^verbatim>\<open>if\<close> or \<^verbatim>\<open>case\<close> statements to set
   21.29 @@ -138,7 +137,7 @@
   21.30  
   21.31    \<^descr>[@{setting ISABELLE_TOOL}\<open>\<^sup>*\<close>] is automatically set to the full path name
   21.32    of the @{executable isabelle} executable. Thus other tools and scripts need
   21.33 -  not assume that the @{dir "$ISABELLE_HOME/bin"} directory is on the current
   21.34 +  not assume that the \<^dir>\<open>$ISABELLE_HOME/bin\<close> directory is on the current
   21.35    search path of the shell.
   21.36  
   21.37    \<^descr>[@{setting_def ISABELLE_IDENTIFIER}\<open>\<^sup>*\<close>] refers to the name of this
   21.38 @@ -147,8 +146,8 @@
   21.39    \<^descr>[@{setting_def ML_SYSTEM}, @{setting_def ML_HOME}, @{setting_def
   21.40    ML_OPTIONS}, @{setting_def ML_PLATFORM}, @{setting_def ML_IDENTIFIER}\<open>\<^sup>*\<close>]
   21.41    specify the underlying ML system to be used for Isabelle. There is only a
   21.42 -  fixed set of admissable @{setting ML_SYSTEM} names (see the @{file
   21.43 -  "$ISABELLE_HOME/etc/settings"} file of the distribution).
   21.44 +  fixed set of admissable @{setting ML_SYSTEM} names (see the
   21.45 +  \<^file>\<open>$ISABELLE_HOME/etc/settings\<close> file of the distribution).
   21.46  
   21.47    The actual compiler binary will be run from the directory @{setting
   21.48    ML_HOME}, with @{setting ML_OPTIONS} as first arguments on the command line.
   21.49 @@ -429,8 +428,8 @@
   21.50    separated by \<open>\<^bold>X\<close>, then split each chunk into sub-chunks separated by \<open>\<^bold>Y\<close>.
   21.51    Markup chunks start with an empty sub-chunk, and a second empty sub-chunk
   21.52    indicates close of an element. Any other non-empty chunk consists of plain
   21.53 -  text. For example, see @{file "~~/src/Pure/PIDE/yxml.ML"} or @{file
   21.54 -  "~~/src/Pure/PIDE/yxml.scala"}.
   21.55 +  text. For example, see \<^file>\<open>~~/src/Pure/PIDE/yxml.ML\<close> or
   21.56 +  \<^file>\<open>~~/src/Pure/PIDE/yxml.scala\<close>.
   21.57  
   21.58    YXML documents may be detected quickly by checking that the first two
   21.59    characters are \<open>\<^bold>X\<^bold>Y\<close>.
    22.1 --- a/src/Doc/System/Misc.thy	Fri Aug 12 17:49:02 2016 +0200
    22.2 +++ b/src/Doc/System/Misc.thy	Fri Aug 12 17:53:55 2016 +0200
    22.3 @@ -34,8 +34,8 @@
    22.4    Components are initialized as described in \secref{sec:components} in a
    22.5    permissive manner, which can mark components as ``missing''. This state is
    22.6    amended by letting @{tool "components"} download and unpack components that
    22.7 -  are published on the default component repository @{url
    22.8 -  "http://isabelle.in.tum.de/components/"} in particular.
    22.9 +  are published on the default component repository
   22.10 +  \<^url>\<open>http://isabelle.in.tum.de/components\<close> in particular.
   22.11  
   22.12    Option \<^verbatim>\<open>-R\<close> specifies an alternative component repository. Note that
   22.13    \<^verbatim>\<open>file:///\<close> URLs can be used for local directories.
    23.1 --- a/src/Doc/System/Presentation.thy	Fri Aug 12 17:49:02 2016 +0200
    23.2 +++ b/src/Doc/System/Presentation.thy	Fri Aug 12 17:53:55 2016 +0200
    23.3 @@ -69,9 +69,9 @@
    23.4    The presentation output will appear in \<^verbatim>\<open>$ISABELLE_BROWSER_INFO/FOL/FOL\<close> as
    23.5    reported by the above verbose invocation of the build process.
    23.6  
    23.7 -  Many Isabelle sessions (such as \<^verbatim>\<open>HOL-Library\<close> in @{dir
    23.8 -  "~~/src/HOL/Library"}) also provide printable documents in PDF. These are
    23.9 -  prepared automatically as well if enabled like this:
   23.10 +  Many Isabelle sessions (such as \<^verbatim>\<open>HOL-Library\<close> in \<^dir>\<open>~~/src/HOL/Library\<close>)
   23.11 +  also provide printable documents in PDF. These are prepared automatically as
   23.12 +  well if enabled like this:
   23.13    @{verbatim [display] \<open>isabelle build -o browser_info -o document=pdf -v -c HOL-Library\<close>}
   23.14  
   23.15    Enabling both browser info and document preparation simultaneously causes an
   23.16 @@ -177,8 +177,8 @@
   23.17    drop, and ``\<^verbatim>\<open>/\<close>\<open>foo\<close>'' to fold text tagged as \<open>foo\<close>. The builtin default is
   23.18    equivalent to the tag specification
   23.19    ``\<^verbatim>\<open>+theory,+proof,+ML,+visible,-invisible\<close>''; see also the {\LaTeX} macros
   23.20 -  \<^verbatim>\<open>\isakeeptag\<close>, \<^verbatim>\<open>\isadroptag\<close>, and \<^verbatim>\<open>\isafoldtag\<close>, in @{file
   23.21 -  "~~/lib/texinputs/isabelle.sty"}.
   23.22 +  \<^verbatim>\<open>\isakeeptag\<close>, \<^verbatim>\<open>\isadroptag\<close>, and \<^verbatim>\<open>\isafoldtag\<close>, in
   23.23 +  \<^file>\<open>~~/lib/texinputs/isabelle.sty\<close>.
   23.24  
   23.25    \<^medskip>
   23.26    Document preparation requires a \<^verbatim>\<open>document\<close> directory within the session
   23.27 @@ -211,8 +211,8 @@
   23.28    user would include \<^verbatim>\<open>session.tex\<close> to get a document containing all the
   23.29    theories.
   23.30  
   23.31 -  The {\LaTeX} versions of the theories require some macros defined in @{file
   23.32 -  "~~/lib/texinputs/isabelle.sty"}. Doing \<^verbatim>\<open>\usepackage{isabelle}\<close> in
   23.33 +  The {\LaTeX} versions of the theories require some macros defined in
   23.34 +  \<^file>\<open>~~/lib/texinputs/isabelle.sty\<close>. Doing \<^verbatim>\<open>\usepackage{isabelle}\<close> in
   23.35    \<^verbatim>\<open>root.tex\<close> should be fine; the underlying @{tool latex} already includes an
   23.36    appropriate path specification for {\TeX} inputs.
   23.37  
   23.38 @@ -221,11 +221,11 @@
   23.39    standard set of {\LaTeX} macro definitions \<^verbatim>\<open>\isasym\<close>\<open>foo\<close> corresponding to
   23.40    \<^verbatim>\<open>\\<close>\<^verbatim>\<open><\<close>\<open>foo\<close>\<^verbatim>\<open>>\<close>, see @{cite "isabelle-implementation"} for a complete list
   23.41    of predefined Isabelle symbols. Users may invent further symbols as well,
   23.42 -  just by providing {\LaTeX} macros in a similar fashion as in @{file
   23.43 -  "~~/lib/texinputs/isabellesym.sty"} of the Isabelle distribution.
   23.44 +  just by providing {\LaTeX} macros in a similar fashion as in
   23.45 +  \<^file>\<open>~~/lib/texinputs/isabellesym.sty\<close> of the Isabelle distribution.
   23.46  
   23.47    For proper setup of DVI and PDF documents (with hyperlinks and bookmarks),
   23.48 -  we recommend to include @{file "~~/lib/texinputs/pdfsetup.sty"} as well.
   23.49 +  we recommend to include \<^file>\<open>~~/lib/texinputs/pdfsetup.sty\<close> as well.
   23.50  
   23.51    \<^medskip>
   23.52    As a final step of Isabelle document preparation, @{tool document}~\<^verbatim>\<open>-c\<close> is
    24.1 --- a/src/Doc/System/Scala.thy	Fri Aug 12 17:49:02 2016 +0200
    24.2 +++ b/src/Doc/System/Scala.thy	Fri Aug 12 17:53:55 2016 +0200
    24.3 @@ -88,8 +88,8 @@
    24.4    This assumes that the executable may be found via the @{setting PATH} from
    24.5    the process environment: this is the case when Isabelle settings are active,
    24.6    e.g.\ in the context of the main Isabelle tool wrapper
    24.7 -  \secref{sec:isabelle-tool}. Alternatively, the full @{file
    24.8 -  "$ISABELLE_HOME/bin/isabelle_scala_script"} may be specified in expanded
    24.9 +  \secref{sec:isabelle-tool}. Alternatively, the full
   24.10 +  \<^file>\<open>$ISABELLE_HOME/bin/isabelle_scala_script\<close> may be specified in expanded
   24.11    form.
   24.12  \<close>
   24.13  
    25.1 --- a/src/Doc/System/Sessions.thy	Fri Aug 12 17:49:02 2016 +0200
    25.2 +++ b/src/Doc/System/Sessions.thy	Fri Aug 12 17:53:55 2016 +0200
    25.3 @@ -140,19 +140,18 @@
    25.4  subsubsection \<open>Examples\<close>
    25.5  
    25.6  text \<open>
    25.7 -  See @{file "~~/src/HOL/ROOT"} for a diversity of practically relevant
    25.8 -  situations, although it uses relatively complex quasi-hierarchic naming
    25.9 -  conventions like \<^verbatim>\<open>HOL-SPARK\<close>, \<^verbatim>\<open>HOL-SPARK-Examples\<close>. An alternative is to
   25.10 -  use unqualified names that are relatively long and descriptive, as in the
   25.11 -  Archive of Formal Proofs (@{url "http://afp.sourceforge.net"}), for
   25.12 -  example.
   25.13 +  See \<^file>\<open>~~/src/HOL/ROOT\<close> for a diversity of practically relevant situations,
   25.14 +  although it uses relatively complex quasi-hierarchic naming conventions like
   25.15 +  \<^verbatim>\<open>HOL-SPARK\<close>, \<^verbatim>\<open>HOL-SPARK-Examples\<close>. An alternative is to use unqualified
   25.16 +  names that are relatively long and descriptive, as in the Archive of Formal
   25.17 +  Proofs (\<^url>\<open>http://afp.sourceforge.net\<close>), for example.
   25.18  \<close>
   25.19  
   25.20  
   25.21  section \<open>System build options \label{sec:system-options}\<close>
   25.22  
   25.23  text \<open>
   25.24 -  See @{file "~~/etc/options"} for the main defaults provided by the Isabelle
   25.25 +  See \<^file>\<open>~~/etc/options\<close> for the main defaults provided by the Isabelle
   25.26    distribution. Isabelle/jEdit @{cite "isabelle-jedit"} includes a simple
   25.27    editing mode \<^verbatim>\<open>isabelle-options\<close> for this file-format.
   25.28  
    26.1 --- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Fri Aug 12 17:49:02 2016 +0200
    26.2 +++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Fri Aug 12 17:53:55 2016 +0200
    26.3 @@ -9152,8 +9152,8 @@
    26.4  
    26.5  subsection \<open>Geometric progression\<close>
    26.6  
    26.7 -text \<open>FIXME: Should one or more of these theorems be moved to @{file
    26.8 -"~~/src/HOL/Set_Interval.thy"}, alongside \<open>geometric_sum\<close>?\<close>
    26.9 +text \<open>FIXME: Should one or more of these theorems be moved to
   26.10 +  \<^file>\<open>~~/src/HOL/Set_Interval.thy\<close>, alongside \<open>geometric_sum\<close>?\<close>
   26.11  
   26.12  lemma sum_gp_basic:
   26.13    fixes x :: "'a::ring_1"
    27.1 --- a/src/HOL/Analysis/Linear_Algebra.thy	Fri Aug 12 17:49:02 2016 +0200
    27.2 +++ b/src/HOL/Analysis/Linear_Algebra.thy	Fri Aug 12 17:53:55 2016 +0200
    27.3 @@ -1654,8 +1654,8 @@
    27.4  qed
    27.5  
    27.6  text \<open>TODO: The following lemmas about adjoints should hold for any
    27.7 -Hilbert space (i.e. complete inner product space).
    27.8 -(see @{url "http://en.wikipedia.org/wiki/Hermitian_adjoint"})
    27.9 +  Hilbert space (i.e. complete inner product space).
   27.10 +  (see \<^url>\<open>http://en.wikipedia.org/wiki/Hermitian_adjoint\<close>)
   27.11  \<close>
   27.12  
   27.13  lemma adjoint_works:
    28.1 --- a/src/HOL/Bali/Decl.thy	Fri Aug 12 17:49:02 2016 +0200
    28.2 +++ b/src/HOL/Bali/Decl.thy	Fri Aug 12 17:53:55 2016 +0200
    28.3 @@ -15,7 +15,7 @@
    28.4  \item clarification and correction of some aspects of the package/access concept
    28.5    (Also submitted as bug report to the Java Bug Database:
    28.6     Bug Id: 4485402 and Bug Id: 4493343 
    28.7 -   @{url "http://developer.java.sun.com/developer/bugParade/index.jshtml"}
    28.8 +   \<^url>\<open>http://developer.java.sun.com/developer/bugParade/index.jshtml\<close>
    28.9    )
   28.10  \end{itemize}
   28.11  simplifications:
    29.1 --- a/src/HOL/Binomial.thy	Fri Aug 12 17:49:02 2016 +0200
    29.2 +++ b/src/HOL/Binomial.thy	Fri Aug 12 17:53:55 2016 +0200
    29.3 @@ -502,7 +502,7 @@
    29.4  
    29.5  subsection \<open>Pochhammer's symbol: generalized rising factorial\<close>
    29.6  
    29.7 -text \<open>See @{url "http://en.wikipedia.org/wiki/Pochhammer_symbol"}\<close>
    29.8 +text \<open>See \<^url>\<open>http://en.wikipedia.org/wiki/Pochhammer_symbol\<close>.\<close>
    29.9  
   29.10  context comm_semiring_1
   29.11  begin
    30.1 --- a/src/HOL/Groups.thy	Fri Aug 12 17:49:02 2016 +0200
    30.2 +++ b/src/HOL/Groups.thy	Fri Aug 12 17:53:55 2016 +0200
    30.3 @@ -602,7 +602,7 @@
    30.4      \<^item> \<^emph>\<open>Partially Ordered Algebraic Systems\<close>, Pergamon Press, 1963
    30.5  
    30.6    Most of the used notions can also be looked up in
    30.7 -    \<^item> @{url "http://www.mathworld.com"} by Eric Weisstein et. al.
    30.8 +    \<^item> \<^url>\<open>http://www.mathworld.com\<close> by Eric Weisstein et. al.
    30.9      \<^item> \<^emph>\<open>Algebra I\<close> by van der Waerden, Springer
   30.10  \<close>
   30.11  
    31.1 --- a/src/HOL/HOLCF/IOA/RefCorrectness.thy	Fri Aug 12 17:49:02 2016 +0200
    31.2 +++ b/src/HOL/HOLCF/IOA/RefCorrectness.thy	Fri Aug 12 17:53:55 2016 +0200
    31.3 @@ -32,7 +32,7 @@
    31.4    Axioms for fair trace inclusion proof support, not for the correctness proof
    31.5    of refinement mappings!
    31.6  
    31.7 -  Note: Everything is superseded by @{file "LiveIOA.thy"}.
    31.8 +  Note: Everything is superseded by \<^file>\<open>LiveIOA.thy\<close>.
    31.9  \<close>
   31.10  
   31.11  axiomatization where
    32.1 --- a/src/HOL/HOLCF/IOA/Traces.thy	Fri Aug 12 17:49:02 2016 +0200
    32.2 +++ b/src/HOL/HOLCF/IOA/Traces.thy	Fri Aug 12 17:53:55 2016 +0200
    32.3 @@ -84,7 +84,7 @@
    32.4    else branch prohibits it. However they can be \<open>sfair\<close> in the case when all
    32.5    \<open>W\<close> are only finitely often enabled: Is this the right model?
    32.6  
    32.7 -  See @{file "LiveIOA.thy"} for solution conforming with the literature and
    32.8 +  See \<^file>\<open>LiveIOA.thy\<close> for solution conforming with the literature and
    32.9    superseding this one.
   32.10  \<close>
   32.11  
    33.1 --- a/src/HOL/Imperative_HOL/Ref.thy	Fri Aug 12 17:49:02 2016 +0200
    33.2 +++ b/src/HOL/Imperative_HOL/Ref.thy	Fri Aug 12 17:53:55 2016 +0200
    33.3 @@ -10,8 +10,8 @@
    33.4  
    33.5  text \<open>
    33.6    Imperative reference operations; modeled after their ML counterparts.
    33.7 -  See @{url "http://caml.inria.fr/pub/docs/manual-caml-light/node14.15.html"}
    33.8 -  and @{url "http://www.smlnj.org/doc/Conversion/top-level-comparison.html"}
    33.9 +  See \<^url>\<open>http://caml.inria.fr/pub/docs/manual-caml-light/node14.15.html\<close>
   33.10 +  and \<^url>\<open>http://www.smlnj.org/doc/Conversion/top-level-comparison.html\<close>.
   33.11  \<close>
   33.12  
   33.13  subsection \<open>Primitives\<close>
    34.1 --- a/src/HOL/Induct/Ordinals.thy	Fri Aug 12 17:49:02 2016 +0200
    34.2 +++ b/src/HOL/Induct/Ordinals.thy	Fri Aug 12 17:53:55 2016 +0200
    34.3 @@ -11,7 +11,7 @@
    34.4  text \<open>
    34.5    Some basic definitions of ordinal numbers.  Draws an Agda
    34.6    development (in Martin-L\"of type theory) by Peter Hancock (see
    34.7 -  @{url "http://www.dcs.ed.ac.uk/home/pgh/chat.html"}).
    34.8 +  \<^url>\<open>http://www.dcs.ed.ac.uk/home/pgh/chat.html\<close>).
    34.9  \<close>
   34.10  
   34.11  datatype ordinal =
    35.1 --- a/src/HOL/Isar_Examples/Cantor.thy	Fri Aug 12 17:49:02 2016 +0200
    35.2 +++ b/src/HOL/Isar_Examples/Cantor.thy	Fri Aug 12 17:53:55 2016 +0200
    35.3 @@ -13,8 +13,8 @@
    35.4  text \<open>
    35.5    Cantor's Theorem states that there is no surjection from
    35.6    a set to its powerset.  The proof works by diagonalization.  E.g.\ see
    35.7 -  \<^item> @{url "http://mathworld.wolfram.com/CantorDiagonalMethod.html"}
    35.8 -  \<^item> @{url "https://en.wikipedia.org/wiki/Cantor's_diagonal_argument"}
    35.9 +  \<^item> \<^url>\<open>http://mathworld.wolfram.com/CantorDiagonalMethod.html\<close>
   35.10 +  \<^item> \<^url>\<open>https://en.wikipedia.org/wiki/Cantor's_diagonal_argument\<close>
   35.11  \<close>
   35.12  
   35.13  theorem Cantor: "\<nexists>f :: 'a \<Rightarrow> 'a set. \<forall>A. \<exists>x. A = f x"
    36.1 --- a/src/HOL/Isar_Examples/Hoare.thy	Fri Aug 12 17:49:02 2016 +0200
    36.2 +++ b/src/HOL/Isar_Examples/Hoare.thy	Fri Aug 12 17:53:55 2016 +0200
    36.3 @@ -16,7 +16,7 @@
    36.4    The following abstract syntax and semantics of Hoare Logic over \<^verbatim>\<open>WHILE\<close>
    36.5    programs closely follows the existing tradition in Isabelle/HOL of
    36.6    formalizing the presentation given in @{cite \<open>\S6\<close> "Winskel:1993"}. See also
    36.7 -  @{dir "~~/src/HOL/Hoare"} and @{cite "Nipkow:1998:Winskel"}.
    36.8 +  \<^dir>\<open>~~/src/HOL/Hoare\<close> and @{cite "Nipkow:1998:Winskel"}.
    36.9  \<close>
   36.10  
   36.11  type_synonym 'a bexp = "'a set"
   36.12 @@ -358,14 +358,14 @@
   36.13  
   36.14  text \<open>
   36.15    We now load the \<^emph>\<open>original\<close> ML file for proof scripts and tactic definition
   36.16 -  for the Hoare Verification Condition Generator (see @{dir
   36.17 -  "~~/src/HOL/Hoare/"}). As far as we are concerned here, the result is a
   36.18 -  proof method \<open>hoare\<close>, which may be applied to a Hoare Logic assertion to
   36.19 -  extract purely logical verification conditions. It is important to note that
   36.20 -  the method requires \<^verbatim>\<open>WHILE\<close> loops to be fully annotated with invariants
   36.21 -  beforehand. Furthermore, only \<^emph>\<open>concrete\<close> pieces of code are handled --- the
   36.22 -  underlying tactic fails ungracefully if supplied with meta-variables or
   36.23 -  parameters, for example.
   36.24 +  for the Hoare Verification Condition Generator (see \<^dir>\<open>~~/src/HOL/Hoare\<close>).
   36.25 +  As far as we are concerned here, the result is a proof method \<open>hoare\<close>, which
   36.26 +  may be applied to a Hoare Logic assertion to extract purely logical
   36.27 +  verification conditions. It is important to note that the method requires
   36.28 +  \<^verbatim>\<open>WHILE\<close> loops to be fully annotated with invariants beforehand.
   36.29 +  Furthermore, only \<^emph>\<open>concrete\<close> pieces of code are handled --- the underlying
   36.30 +  tactic fails ungracefully if supplied with meta-variables or parameters, for
   36.31 +  example.
   36.32  \<close>
   36.33  
   36.34  lemma SkipRule: "p \<subseteq> q \<Longrightarrow> Valid p (Basic id) q"
    37.1 --- a/src/HOL/Isar_Examples/Schroeder_Bernstein.thy	Fri Aug 12 17:49:02 2016 +0200
    37.2 +++ b/src/HOL/Isar_Examples/Schroeder_Bernstein.thy	Fri Aug 12 17:53:55 2016 +0200
    37.3 @@ -10,8 +10,8 @@
    37.4  
    37.5  text \<open>
    37.6    See also:
    37.7 -  \<^item> @{file "$ISABELLE_HOME/src/HOL/ex/Set_Theory.thy"}
    37.8 -  \<^item> @{url "http://planetmath.org/proofofschroederbernsteintheoremusingtarskiknastertheorem"}
    37.9 +  \<^item> \<^file>\<open>$ISABELLE_HOME/src/HOL/ex/Set_Theory.thy\<close>
   37.10 +  \<^item> \<^url>\<open>http://planetmath.org/proofofschroederbernsteintheoremusingtarskiknastertheorem\<close>
   37.11    \<^item> Springer LNCS 828 (cover page)
   37.12  \<close>
   37.13  
    38.1 --- a/src/HOL/Library/Code_Test.thy	Fri Aug 12 17:49:02 2016 +0200
    38.2 +++ b/src/HOL/Library/Code_Test.thy	Fri Aug 12 17:53:55 2016 +0200
    38.3 @@ -53,9 +53,10 @@
    38.4    and (Scala) "_.mkString(\"\")"
    38.5  
    38.6  text \<open>
    38.7 -  Stripped-down implementations of Isabelle's XML tree with YXML encoding
    38.8 -  as defined in @{file "~~/src/Pure/PIDE/xml.ML"}, @{file "~~/src/Pure/PIDE/yxml.ML"}
    38.9 -  sufficient to encode @{typ "Code_Evaluation.term"} as in @{file "~~/src/Pure/term_xml.ML"}.
   38.10 +  Stripped-down implementations of Isabelle's XML tree with YXML encoding as
   38.11 +  defined in \<^file>\<open>~~/src/Pure/PIDE/xml.ML\<close>, \<^file>\<open>~~/src/Pure/PIDE/yxml.ML\<close>
   38.12 +  sufficient to encode @{typ "Code_Evaluation.term"} as in
   38.13 +  \<^file>\<open>~~/src/Pure/term_xml.ML\<close>.
   38.14  \<close>
   38.15  
   38.16  datatype (plugins del: code size "quickcheck") xml_tree = XML_Tree
   38.17 @@ -113,8 +114,8 @@
   38.18  where "yxml_string_of_body ts = foldr yxml_string_of_xml_tree ts yot_empty"
   38.19  
   38.20  text \<open>
   38.21 -  Encoding @{typ Code_Evaluation.term} into XML trees
   38.22 -  as defined in @{file "~~/src/Pure/term_xml.ML"}
   38.23 +  Encoding @{typ Code_Evaluation.term} into XML trees as defined in
   38.24 +  \<^file>\<open>~~/src/Pure/term_xml.ML\<close>.
   38.25  \<close>
   38.26  
   38.27  definition xml_of_typ :: "Typerep.typerep \<Rightarrow> xml.body"
    39.1 --- a/src/HOL/Library/Extended_Real.thy	Fri Aug 12 17:49:02 2016 +0200
    39.2 +++ b/src/HOL/Library/Extended_Real.thy	Fri Aug 12 17:53:55 2016 +0200
    39.3 @@ -218,10 +218,8 @@
    39.4  qed
    39.5  
    39.6  text \<open>
    39.7 -
    39.8 -For more lemmas about the extended real numbers go to
    39.9 -  @{file "~~/src/HOL/Analysis/Extended_Real_Limits.thy"}
   39.10 -
   39.11 +  For more lemmas about the extended real numbers see
   39.12 +  \<^file>\<open>~~/src/HOL/Analysis/Extended_Real_Limits.thy\<close>.
   39.13  \<close>
   39.14  
   39.15  subsection \<open>Definition and basic properties\<close>
    40.1 --- a/src/HOL/Library/RBT_Impl.thy	Fri Aug 12 17:49:02 2016 +0200
    40.2 +++ b/src/HOL/Library/RBT_Impl.thy	Fri Aug 12 17:53:55 2016 +0200
    40.3 @@ -551,8 +551,10 @@
    40.4  lemma bheight_paintR'[simp]: "color_of t = B \<Longrightarrow> bheight (paint R t) = bheight t - 1"
    40.5  by (cases t rule: rbt_cases) auto
    40.6  
    40.7 -text \<open>The function definitions are based on the Haskell code by Stefan Kahrs
    40.8 -at @{url "http://www.cs.ukc.ac.uk/people/staff/smk/redblack/rb.html"} .\<close>
    40.9 +text \<open>
   40.10 +  The function definitions are based on the Haskell code by Stefan Kahrs
   40.11 +  at \<^url>\<open>http://www.cs.ukc.ac.uk/people/staff/smk/redblack/rb.html\<close>.
   40.12 +\<close>
   40.13  
   40.14  fun
   40.15    balance_left :: "('a,'b) rbt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"
    41.1 --- a/src/HOL/Library/Set_Algebras.thy	Fri Aug 12 17:49:02 2016 +0200
    41.2 +++ b/src/HOL/Library/Set_Algebras.thy	Fri Aug 12 17:53:55 2016 +0200
    41.3 @@ -13,7 +13,7 @@
    41.4  text \<open>
    41.5    This library lifts operations like addition and multiplication to sets. It
    41.6    was designed to support asymptotic calculations. See the comments at the top
    41.7 -  of @{file "BigO.thy"}.
    41.8 +  of \<^file>\<open>BigO.thy\<close>.
    41.9  \<close>
   41.10  
   41.11  instantiation set :: (plus) plus
    42.1 --- a/src/HOL/Library/State_Monad.thy	Fri Aug 12 17:49:02 2016 +0200
    42.2 +++ b/src/HOL/Library/State_Monad.thy	Fri Aug 12 17:53:55 2016 +0200
    42.3 @@ -20,7 +20,7 @@
    42.4    monads}, since a state is transformed single-threadedly).
    42.5  
    42.6    To enter from the Haskell world,
    42.7 -  @{url "http://www.engr.mun.ca/~theo/Misc/haskell_and_monads.htm"} makes
    42.8 +  \<^url>\<open>http://www.engr.mun.ca/~theo/Misc/haskell_and_monads.htm\<close> makes
    42.9    a good motivating start.  Here we just sketch briefly how those
   42.10    monads enter the game of Isabelle/HOL.
   42.11  \<close>
   42.12 @@ -145,7 +145,7 @@
   42.13    "_sdo_block (_sdo_final e)" => "e"
   42.14  
   42.15  text \<open>
   42.16 -  For an example, see @{file "~~/src/HOL/Proofs/Extraction/Higman_Extraction.thy"}.
   42.17 +  For an example, see \<^file>\<open>~~/src/HOL/Proofs/Extraction/Higman_Extraction.thy\<close>.
   42.18  \<close>
   42.19  
   42.20  end
    43.1 --- a/src/HOL/Nominal/Examples/CK_Machine.thy	Fri Aug 12 17:49:02 2016 +0200
    43.2 +++ b/src/HOL/Nominal/Examples/CK_Machine.thy	Fri Aug 12 17:53:55 2016 +0200
    43.3 @@ -16,9 +16,8 @@
    43.4    by Roshan James (Indiana University) and also by the lecture notes 
    43.5    written by Andy Pitts for his semantics course. See
    43.6    
    43.7 -     @{url "http://www.cs.indiana.edu/~rpjames/lm.pdf"}
    43.8 -     @{url "http://www.cl.cam.ac.uk/teaching/2001/Semantics/"}
    43.9 -
   43.10 +     \<^url>\<open>http://www.cs.indiana.edu/~rpjames/lm.pdf\<close>
   43.11 +     \<^url>\<open>http://www.cl.cam.ac.uk/teaching/2001/Semantics\<close>
   43.12  \<close>
   43.13  
   43.14  atom_decl name
    44.1 --- a/src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy	Fri Aug 12 17:49:02 2016 +0200
    44.2 +++ b/src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy	Fri Aug 12 17:53:55 2016 +0200
    44.3 @@ -4,7 +4,7 @@
    44.4    "~~/src/HOL/Library/Code_Prolog"
    44.5  begin
    44.6  
    44.7 -text \<open>An example from the experiments from SmallCheck (@{url "http://www.cs.york.ac.uk/fp/smallcheck/"})\<close>
    44.8 +text \<open>An example from the experiments from SmallCheck (\<^url>\<open>http://www.cs.york.ac.uk/fp/smallcheck\<close>)\<close>
    44.9  text \<open>The example (original in Haskell) was imported with Haskabelle and
   44.10    manually slightly adapted.
   44.11  \<close>
    45.1 --- a/src/HOL/Probability/Probability_Mass_Function.thy	Fri Aug 12 17:49:02 2016 +0200
    45.2 +++ b/src/HOL/Probability/Probability_Mass_Function.thy	Fri Aug 12 17:53:55 2016 +0200
    45.3 @@ -1414,7 +1414,7 @@
    45.4    Proof that @{const rel_pmf} preserves orders.
    45.5    Antisymmetry proof follows Thm. 1 in N. Saheb-Djahromi, Cpo's of measures for nondeterminism,
    45.6    Theoretical Computer Science 12(1):19--37, 1980,
    45.7 -  @{url "http://dx.doi.org/10.1016/0304-3975(80)90003-1"}
    45.8 +  \<^url>\<open>http://dx.doi.org/10.1016/0304-3975(80)90003-1\<close>
    45.9  \<close>
   45.10  
   45.11  lemma
    46.1 --- a/src/HOL/Real.thy	Fri Aug 12 17:49:02 2016 +0200
    46.2 +++ b/src/HOL/Real.thy	Fri Aug 12 17:53:55 2016 +0200
    46.3 @@ -14,10 +14,10 @@
    46.4  begin
    46.5  
    46.6  text \<open>
    46.7 -  This theory contains a formalization of the real numbers as
    46.8 -  equivalence classes of Cauchy sequences of rationals.  See
    46.9 -  @{file "~~/src/HOL/ex/Dedekind_Real.thy"} for an alternative
   46.10 -  construction using Dedekind cuts.
   46.11 +  This theory contains a formalization of the real numbers as equivalence
   46.12 +  classes of Cauchy sequences of rationals. See
   46.13 +  \<^file>\<open>~~/src/HOL/ex/Dedekind_Real.thy\<close> for an alternative construction using
   46.14 +  Dedekind cuts.
   46.15  \<close>
   46.16  
   46.17  
    47.1 --- a/src/HOL/Real_Vector_Spaces.thy	Fri Aug 12 17:49:02 2016 +0200
    47.2 +++ b/src/HOL/Real_Vector_Spaces.thy	Fri Aug 12 17:53:55 2016 +0200
    47.3 @@ -2084,7 +2084,7 @@
    47.4  
    47.5  text \<open>
    47.6    Proof that Cauchy sequences converge based on the one from
    47.7 -  @{url "http://pirate.shu.edu/~wachsmut/ira/numseq/proofs/cauconv.html"}
    47.8 +  \<^url>\<open>http://pirate.shu.edu/~wachsmut/ira/numseq/proofs/cauconv.html\<close>
    47.9  \<close>
   47.10  
   47.11  text \<open>
    48.1 --- a/src/HOL/Rings.thy	Fri Aug 12 17:49:02 2016 +0200
    48.2 +++ b/src/HOL/Rings.thy	Fri Aug 12 17:53:55 2016 +0200
    48.3 @@ -538,7 +538,7 @@
    48.4      \<^item> \<^emph>\<open>Partially Ordered Algebraic Systems\<close>, Pergamon Press, 1963
    48.5  
    48.6    Most of the used notions can also be looked up in
    48.7 -    \<^item> @{url "http://www.mathworld.com"} by Eric Weisstein et. al.
    48.8 +    \<^item> \<^url>\<open>http://www.mathworld.com\<close> by Eric Weisstein et. al.
    48.9      \<^item> \<^emph>\<open>Algebra I\<close> by van der Waerden, Springer
   48.10  \<close>
   48.11  
    49.1 --- a/src/HOL/Series.thy	Fri Aug 12 17:49:02 2016 +0200
    49.2 +++ b/src/HOL/Series.thy	Fri Aug 12 17:53:55 2016 +0200
    49.3 @@ -817,7 +817,7 @@
    49.4  
    49.5  text \<open>
    49.6    Proof based on Analysis WebNotes: Chapter 07, Class 41
    49.7 -  @{url "http://www.math.unl.edu/~webnotes/classes/class41/prp77.htm"}
    49.8 +  \<^url>\<open>http://www.math.unl.edu/~webnotes/classes/class41/prp77.htm\<close>
    49.9  \<close>
   49.10  
   49.11  lemma Cauchy_product_sums:
    50.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Fri Aug 12 17:49:02 2016 +0200
    50.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Fri Aug 12 17:53:55 2016 +0200
    50.3 @@ -199,10 +199,10 @@
    50.4  (** invocation of Haskell interpreter **)
    50.5  
    50.6  val narrowing_engine =
    50.7 -  File.read @{file "~~/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs"}
    50.8 +  File.read \<^file>\<open>~~/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs\<close>
    50.9  
   50.10  val pnf_narrowing_engine =
   50.11 -  File.read @{file "~~/src/HOL/Tools/Quickcheck/PNF_Narrowing_Engine.hs"}
   50.12 +  File.read \<^file>\<open>~~/src/HOL/Tools/Quickcheck/PNF_Narrowing_Engine.hs\<close>
   50.13  
   50.14  fun exec verbose code =
   50.15    ML_Context.exec (fn () =>
    51.1 --- a/src/HOL/Word/Word.thy	Fri Aug 12 17:49:02 2016 +0200
    51.2 +++ b/src/HOL/Word/Word.thy	Fri Aug 12 17:53:55 2016 +0200
    51.3 @@ -14,7 +14,7 @@
    51.4    Word_Miscellaneous
    51.5  begin
    51.6  
    51.7 -text \<open>See @{file "Examples/WordExamples.thy"} for examples.\<close>
    51.8 +text \<open>See \<^file>\<open>Examples/WordExamples.thy\<close> for examples.\<close>
    51.9  
   51.10  subsection \<open>Type definition\<close>
   51.11  
    52.1 --- a/src/HOL/ex/ML.thy	Fri Aug 12 17:49:02 2016 +0200
    52.2 +++ b/src/HOL/ex/ML.thy	Fri Aug 12 17:53:55 2016 +0200
    52.3 @@ -94,7 +94,7 @@
    52.4  ML \<open>factorial 42\<close>
    52.5  ML \<open>factorial 10000 div factorial 9999\<close>
    52.6  
    52.7 -text \<open>See @{url "http://mathworld.wolfram.com/AckermannFunction.html"}\<close>
    52.8 +text \<open>See \<^url>\<open>http://mathworld.wolfram.com/AckermannFunction.html\<close>.\<close>
    52.9  
   52.10  ML \<open>
   52.11    fun ackermann 0 n = n + 1
    53.1 --- a/src/HOL/ex/NatSum.thy	Fri Aug 12 17:49:02 2016 +0200
    53.2 +++ b/src/HOL/ex/NatSum.thy	Fri Aug 12 17:53:55 2016 +0200
    53.3 @@ -10,7 +10,7 @@
    53.4    Summing natural numbers, squares, cubes, etc.
    53.5  
    53.6    Thanks to Sloane's On-Line Encyclopedia of Integer Sequences,
    53.7 -  @{url "http://www.research.att.com/~njas/sequences/"}.
    53.8 +  \<^url>\<open>http://www.research.att.com/~njas/sequences\<close>.
    53.9  \<close>
   53.10  
   53.11  lemmas [simp] =
    54.1 --- a/src/HOL/ex/Simproc_Tests.thy	Fri Aug 12 17:49:02 2016 +0200
    54.2 +++ b/src/HOL/ex/Simproc_Tests.thy	Fri Aug 12 17:53:55 2016 +0200
    54.3 @@ -9,10 +9,9 @@
    54.4  begin
    54.5  
    54.6  text \<open>
    54.7 -  This theory tests the various simprocs defined in @{file
    54.8 -  "~~/src/HOL/Nat.thy"} and @{file "~~/src/HOL/Numeral_Simprocs.thy"}.
    54.9 -  Many of the tests are derived from commented-out code originally
   54.10 -  found in @{file "~~/src/HOL/Tools/numeral_simprocs.ML"}.
   54.11 +  This theory tests the various simprocs defined in \<^file>\<open>~~/src/HOL/Nat.thy\<close> and
   54.12 +  \<^file>\<open>~~/src/HOL/Numeral_Simprocs.thy\<close>. Many of the tests are derived from commented-out code
   54.13 +  originally found in \<^file>\<open>~~/src/HOL/Tools/numeral_simprocs.ML\<close>.
   54.14  \<close>
   54.15  
   54.16  subsection \<open>ML bindings\<close>
    55.1 --- a/src/HOL/ex/Sudoku.thy	Fri Aug 12 17:49:02 2016 +0200
    55.2 +++ b/src/HOL/ex/Sudoku.thy	Fri Aug 12 17:53:55 2016 +0200
    55.3 @@ -136,7 +136,7 @@
    55.4  
    55.5  text \<open>
    55.6    Some ``exceptionally difficult'' Sudokus, taken from
    55.7 -  @{url "http://en.wikipedia.org/w/index.php?title=Algorithmics_of_sudoku&oldid=254685903"}
    55.8 +  \<^url>\<open>http://en.wikipedia.org/w/index.php?title=Algorithmics_of_sudoku&oldid=254685903\<close>
    55.9    (accessed December~2, 2008).
   55.10  \<close>
   55.11  
    56.1 --- a/src/Pure/Tools/jedit.ML	Fri Aug 12 17:49:02 2016 +0200
    56.2 +++ b/src/Pure/Tools/jedit.ML	Fri Aug 12 17:53:55 2016 +0200
    56.3 @@ -24,13 +24,13 @@
    56.4  
    56.5  val isabelle_jedit_actions =
    56.6    Lazy.lazy (fn () =>
    56.7 -    (case XML.parse (File.read @{file "~~/src/Tools/jEdit/src/actions.xml"}) of
    56.8 +    (case XML.parse (File.read \<^file>\<open>~~/src/Tools/jEdit/src/actions.xml\<close>) of
    56.9        XML.Elem (("ACTIONS", _), body) => maps (parse_named "ACTION") body
   56.10      | _ => []));
   56.11  
   56.12  val isabelle_jedit_dockables =
   56.13    Lazy.lazy (fn () =>
   56.14 -    (case XML.parse (File.read @{file "~~/src/Tools/jEdit/src/dockables.xml"}) of
   56.15 +    (case XML.parse (File.read \<^file>\<open>~~/src/Tools/jEdit/src/dockables.xml\<close>) of
   56.16        XML.Elem (("DOCKABLES", _), body) => maps (parse_named "DOCKABLE") body
   56.17      | _ => []));
   56.18