# HG changeset patch
# User immler
# Date 1572224158 14400
# Node ID ba0b65d45aec53910020f8cfa117314079e3c054
# Parent  e8fc52f3f175c36d5b1dd0f0835ce987e1665f4b
header with Title/Author; added note on motivation of this example

diff -r e8fc52f3f175 -r ba0b65d45aec src/HOL/Eisbach/Example_Metric.thy
--- a/src/HOL/Eisbach/Example_Metric.thy	Sun Oct 27 20:53:10 2019 -0400
+++ b/src/HOL/Eisbach/Example_Metric.thy	Sun Oct 27 20:55:58 2019 -0400
@@ -1,7 +1,13 @@
+(*  Title:    Example_Metric.thy
+    Author:   Maximilian Schäffeler
+*)
 theory Example_Metric
   imports "HOL-Analysis.Metric_Arith" "HOL-Eisbach.Eisbach_Tools"
 begin
 
+text \<open>An Eisbach implementation of the method @{method metric}.
+  Slower than the Isabelle/ML implementation but arguably more readable.\<close>
+
 method dist_refl_sym = simp only: simp_thms dist_commute dist_self
 
 method lin_real_arith uses thms = argo thms