--- a/src/Doc/Isar_Ref/Spec.thy Thu Jan 05 21:18:55 2023 +0100
+++ b/src/Doc/Isar_Ref/Spec.thy Thu Jan 05 21:33:49 2023 +0100
@@ -1324,8 +1324,8 @@
files as for \<^theory_text>\<open>export_generated_files\<close> and writes them into a temporary
directory, which is taken as starting point for build process of
Isabelle/Scala/Java modules (see @{cite "isabelle-system"}). The
- corresponding @{path build.props} file is expected directly in the toplevel
- directory, instead of @{path "etc/build.props"} for Isabelle system
+ corresponding @{path \<open>build.props\<close>} file is expected directly in the toplevel
+ directory, instead of @{path \<open>etc/build.props\<close>} for Isabelle system
components. These properties need to specify sources, resources, services
etc. as usual. The resulting JAR module becomes an export artefact of the
session database, with a name of the form
--- a/src/HOL/Analysis/Metric_Arith.thy Thu Jan 05 21:18:55 2023 +0100
+++ b/src/HOL/Analysis/Metric_Arith.thy Thu Jan 05 21:33:49 2023 +0100
@@ -105,7 +105,7 @@
"x \<in> s \<Longrightarrow> y \<in> s \<Longrightarrow> x = y \<longleftrightarrow> (\<forall>a\<in>s. dist x a = dist y a)"
by auto
-ML_file "metric_arith.ML"
+ML_file \<open>metric_arith.ML\<close>
method_setup metric = \<open>
Scan.succeed (SIMPLE_METHOD' o Metric_Arith.metric_arith_tac)
--- a/src/HOL/Quotient.thy Thu Jan 05 21:18:55 2023 +0100
+++ b/src/HOL/Quotient.thy Thu Jan 05 21:33:49 2023 +0100
@@ -870,7 +870,7 @@
unfolding Quotient_def eq_onp_def
by unfold_locales auto
-ML_file "Tools/BNF/bnf_lift.ML"
+ML_file \<open>Tools/BNF/bnf_lift.ML\<close>
hide_fact
sum_insert_Inl_unit lift_sum_unit_vimage_commute insert_Inl_int_map_sum_unit
--- a/src/Pure/Pure.thy Thu Jan 05 21:18:55 2023 +0100
+++ b/src/Pure/Pure.thy Thu Jan 05 21:33:49 2023 +0100
@@ -202,8 +202,8 @@
(Toplevel.context_of st) args external)));
in end\<close>
-external_file "ROOT0.ML"
-external_file "ROOT.ML"
+external_file \<open>ROOT0.ML\<close>
+external_file \<open>ROOT.ML\<close>
subsection \<open>Embedded ML text\<close>