Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Analysis/Metric_Arith.thy
changeset 76923 8a66a88cd5dc
parent 74546 6df92c387063
child 76987 4c275405faae 
--- 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)
isabelle