src/Doc/Datatypes/Datatypes.thy

 allow infinite paths. Orthogonally, the nodes in the first and third types have
 finitely many direct subtrees, whereas those of the second and fourth may have
 infinite branching.
 
 The package is part of @{theory Main}. Additional functionality is provided by
-the theory @{file "~~/src/HOL/Library/BNF_Axiomatization.thy"}.
+the theory \<^file>\<open>~~/src/HOL/Library/BNF_Axiomatization.thy\<close>.
 
 The package, like its predecessor, fully adheres to the LCF philosophy
 @{cite mgordon79}: The characteristic theorems associated with the specified
 (co)datatypes are derived rather than introduced axiomatically.%
 \footnote{However, some of the

   \label{ssec:datatype-introductory-examples}\<close>
 
 text \<open>
 Datatypes are illustrated through concrete examples featuring different flavors
 of recursion. More examples can be found in the directory
-@{dir "~~/src/HOL/Datatype_Examples"}.
+\<^dir>\<open>~~/src/HOL/Datatype_Examples\<close>.
 \<close>
 
 
 subsubsection \<open>Nonrecursive Types
   \label{sssec:datatype-nonrecursive-types}\<close>

 
 subsubsection \<open>\textit{countable_datatype}
   \label{sssec:datatype-compat}\<close>
 
 text \<open>
-The theory @{file "~~/src/HOL/Library/Countable.thy"} provides a
+The theory \<^file>\<open>~~/src/HOL/Library/Countable.thy\<close> provides a
 proof method called @{method countable_datatype} that can be used to prove the
 countability of many datatypes, building on the countability of the types
 appearing in their definitions and of any type arguments. For example:
 \<close>
 

 @{text "[where \<dots>]"} attribute. The solution is to use the more robust
 @{text "[of \<dots>]"} syntax.
 \end{itemize}
 
 The old command is still available as \keyw{old_datatype} in theory
-@{file "~~/src/HOL/Library/Old_Datatype.thy"}. However, there is no general
+\<^file>\<open>~~/src/HOL/Library/Old_Datatype.thy\<close>. However, there is no general
 way to register old-style datatypes as new-style datatypes. If the objective
 is to define new-style datatypes with nested recursion through old-style
 datatypes, the old-style datatypes can be registered as a BNF
 (Section~\ref{sec:registering-bounded-natural-functors}). If the objective is
 to derive discriminators and selectors, this can be achieved using

   \label{ssec:primrec-introductory-examples}\<close>
 
 text \<open>
 Primitive recursion is illustrated through concrete examples based on the
 datatypes defined in Section~\ref{ssec:datatype-introductory-examples}. More
-examples can be found in the directory @{dir "~~/src/HOL/Datatype_Examples"}.
+examples can be found in the directory \<^dir>\<open>~~/src/HOL/Datatype_Examples\<close>.
 \<close>
 
 
 subsubsection \<open>Nonrecursive Types
   \label{sssec:primrec-nonrecursive-types}\<close>

 text \<open>
 \noindent
 Pattern matching is only available for the argument on which the recursion takes
 place. Fortunately, it is easy to generate pattern-maching equations using the
 @{command simps_of_case} command provided by the theory
-@{file "~~/src/HOL/Library/Simps_Case_Conv.thy"}.
+\<^file>\<open>~~/src/HOL/Library/Simps_Case_Conv.thy\<close>.
 \<close>
 
     simps_of_case at_simps_alt: at.simps
 
 text \<open>

 
 text \<open>
 Codatatypes can be specified using the @{command codatatype} command. The
 command is first illustrated through concrete examples featuring different
 flavors of corecursion. More examples can be found in the directory
-@{dir "~~/src/HOL/Datatype_Examples"}. The \emph{Archive of Formal Proofs} also
+\<^dir>\<open>~~/src/HOL/Datatype_Examples\<close>. The \emph{Archive of Formal Proofs} also
 includes some useful codatatypes, notably for lazy lists @{cite
 "lochbihler-2010"}.
 \<close>
 
 

 \keyw{corec} and \keyw{corecursive} commands, and techniques based on domains
 and topologies @{cite "lochbihler-hoelzl-2014"}. In this tutorial, the focus is
 on @{command primcorec} and @{command primcorecursive}; \keyw{corec} and
 \keyw{corecursive} are described in a separate tutorial
 @{cite "isabelle-corec"}. More examples can be found in the directories
-@{dir "~~/src/HOL/Datatype_Examples"} and @{dir "~~/src/HOL/Corec_Examples"}.
+\<^dir>\<open>~~/src/HOL/Datatype_Examples\<close> and \<^dir>\<open>~~/src/HOL/Corec_Examples\<close>.
 
 Whereas recursive functions consume datatypes one constructor at a time,
 corecursive functions construct codatatypes one constructor at a time.
 Partly reflecting a lack of agreement among proponents of coalgebraic methods,
 Isabelle supports three competing syntaxes for specifying a function $f$:

   \label{ssec:primcorec-introductory-examples}\<close>
 
 text \<open>
 Primitive corecursion is illustrated through concrete examples based on the
 codatatypes defined in Section~\ref{ssec:codatatype-introductory-examples}. More
-examples can be found in the directory @{dir "~~/src/HOL/Datatype_Examples"}.
+examples can be found in the directory \<^dir>\<open>~~/src/HOL/Datatype_Examples\<close>.
 The code view is favored in the examples below. Sections
 \ref{ssec:primrec-constructor-view} and \ref{ssec:primrec-destructor-view}
 present the same examples expressed using the constructor and destructor views.
 \<close>
 

 For technical reasons, @{text "case"}--@{text "of"} is only supported for
 case distinctions on (co)datatypes that provide discriminators and selectors.
 
 Pattern matching is not supported by @{command primcorec}. Fortunately, it is
 easy to generate pattern-maching equations using the @{command simps_of_case}
-command provided by the theory @{file "~~/src/HOL/Library/Simps_Case_Conv.thy"}.
+command provided by the theory \<^file>\<open>~~/src/HOL/Library/Simps_Case_Conv.thy\<close>.
 \<close>
 
     simps_of_case lapp_simps: lapp.code
 
 text \<open>

   \label{ssec:bnf-introductory-examples}\<close>
 
 text \<open>
 The example below shows how to register a type as a BNF using the @{command bnf}
 command. Some of the proof obligations are best viewed with the theory
-@{file "~~/src/HOL/Library/Cardinal_Notations.thy"} imported.
+\<^file>\<open>~~/src/HOL/Library/Cardinal_Notations.thy\<close> imported.
 
 The type is simply a copy of the function space @{typ "'d \<Rightarrow> 'a"}, where @{typ 'a}
 is live and @{typ 'd} is dead. We introduce it together with its map function,
 set function, predicator, and relator.
 \<close>

 Using \keyw{print_theorems} and @{command print_bnfs}, we can contemplate and
 show the world what we have achieved.
 
 This particular example does not need any nonemptiness witness, because the
 one generated by default is good enough, but in general this would be
-necessary. See @{file "~~/src/HOL/Basic_BNFs.thy"},
-@{file "~~/src/HOL/Library/Countable_Set_Type.thy"},
-@{file "~~/src/HOL/Library/FSet.thy"}, and
-@{file "~~/src/HOL/Library/Multiset.thy"} for further examples of BNF
+necessary. See \<^file>\<open>~~/src/HOL/Basic_BNFs.thy\<close>,
+\<^file>\<open>~~/src/HOL/Library/Countable_Set_Type.thy\<close>,
+\<^file>\<open>~~/src/HOL/Library/FSet.thy\<close>, and
+\<^file>\<open>~~/src/HOL/Library/Multiset.thy\<close> for further examples of BNF
 registration, some of which feature custom witnesses.
 
 For many typedefs, lifting the BNF structure from the raw type to the abstract
 type can be done uniformly. This is the task of the @{command lift_bnf} command.
 Using @{command lift_bnf}, the above registration of @{typ "('d, 'a) fn"} as a

 is identical to the left-hand side of a @{command datatype} or
 @{command codatatype} definition.
 
 The command is useful to reason abstractly about BNFs. The axioms are safe
 because there exist BNFs of arbitrary large arities. Applications must import
-the @{file "~~/src/HOL/Library/BNF_Axiomatization.thy"} theory
+the \<^file>\<open>~~/src/HOL/Library/BNF_Axiomatization.thy\<close> theory
 to use this functionality.
 \<close>
 
 
 subsubsection \<open>\keyw{print_bnfs}

 
 \medskip
 
 \noindent
 The @{command simps_of_case} command provided by theory
-@{file "~~/src/HOL/Library/Simps_Case_Conv.thy"} converts a single equation with
+\<^file>\<open>~~/src/HOL/Library/Simps_Case_Conv.thy\<close> converts a single equation with
 a complex case expression on the right-hand side into a set of pattern-matching
 equations. For example,
 \<close>
 
 (*<*)

 
 \medskip
 
 \noindent
 The \keyw{case_of_simps} command provided by theory
-@{file "~~/src/HOL/Library/Simps_Case_Conv.thy"} converts a set of
+\<^file>\<open>~~/src/HOL/Library/Simps_Case_Conv.thy\<close> converts a set of
 pattern-matching equations into single equation with a complex case expression
 on the right-hand side (cf.\ @{command simps_of_case}). For example,
 \<close>
 
     case_of_simps lapp_case: lapp_simps

 @{text "'a\<^sub>1, \<dots>, 'a\<^sub>m"}, by default @{text u} values are given a size of 0. This
 can be improved upon by registering a custom size function of type
 @{text "('a\<^sub>1 \<Rightarrow> nat) \<Rightarrow> \<dots> \<Rightarrow> ('a\<^sub>m \<Rightarrow> nat) \<Rightarrow> u \<Rightarrow> nat"} using
 the ML function @{ML BNF_LFP_Size.register_size} or
 @{ML BNF_LFP_Size.register_size_global}. See theory
-@{file "~~/src/HOL/Library/Multiset.thy"} for an example.
+\<^file>\<open>~~/src/HOL/Library/Multiset.thy\<close> for an example.
 \<close>
 
 
 subsection \<open>Transfer
   \label{ssec:transfer}\<close>