--- 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
--- 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