# HG changeset patch
# User wenzelm
# Date 1634648580 -7200
# Node ID 6df92c38706394e21600a91f7bfd50d8872d890d
# Parent  6c123914883ab4f7b6c827c7f0146df85d627fbe
proper file headers;

diff -r 6c123914883a -r 6df92c387063 src/HOL/Analysis/Metric_Arith.thy
--- a/src/HOL/Analysis/Metric_Arith.thy	Tue Oct 19 14:58:22 2021 +0200
+++ b/src/HOL/Analysis/Metric_Arith.thy	Tue Oct 19 15:03:00 2021 +0200
@@ -1,5 +1,5 @@
-(*  Title:    Metric_Arith.thy
-    Author:   Maximilian Schäffeler (port from HOL Light)
+(*  Title:      HOL/Analysis/Metric_Arith.thy
+    Author:     Maximilian Schäffeler (port from HOL Light)
 *)
 
 chapter \<open>Functional Analysis\<close>
@@ -108,7 +108,7 @@
 ML_file "metric_arith.ML"
 
 method_setup metric = \<open>
-  Scan.succeed (SIMPLE_METHOD' o MetricArith.metric_arith_tac)
+  Scan.succeed (SIMPLE_METHOD' o Metric_Arith.metric_arith_tac)
 \<close> "prove simple linear statements in metric spaces (\<forall>\<exists>\<^sub>p fragment)"
 
-end
\ No newline at end of file
+end
diff -r 6c123914883a -r 6df92c387063 src/HOL/Analysis/metric_arith.ML
--- a/src/HOL/Analysis/metric_arith.ML	Tue Oct 19 14:58:22 2021 +0200
+++ b/src/HOL/Analysis/metric_arith.ML	Tue Oct 19 15:03:00 2021 +0200
@@ -1,9 +1,17 @@
-signature METRIC_ARITH = sig
+(*  Title:      HOL/Analysis/metric_arith.ML
+    Author:     Maximilian Schäffeler (port from HOL Light)
+
+A decision procedure for metric spaces.
+*)
+
+signature METRIC_ARITH =
+sig
+  val trace: bool Config.T
   val metric_arith_tac : Proof.context -> int -> tactic
-  val trace: bool Config.T
 end
 
-structure MetricArith : METRIC_ARITH = struct
+structure Metric_Arith : METRIC_ARITH =
+struct
 
 fun default d x = case x of SOME y => SOME y | NONE => d
 
@@ -318,4 +326,5 @@
   IF_UNSOLVED' (SUBPROOF (fn {context=ctxt', ...} =>
     trace_tac ctxt' "Focused on subgoal" THEN
     elim_exists ctxt') ctxt)
+
 end