Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
header with Title/Author; added note on motivation of this example
authorimmler
Sun, 27 Oct 2019 20:55:58 -0400
changeset 70959 ba0b65d45aec
parent 70958 e8fc52f3f175
child 70960 84f79d82df0a
header with Title/Author; added note on motivation of this example
src/HOL/Eisbach/Example_Metric.thy file | annotate | diff | comparison | revisions 
--- 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
isabelle