Changes

Summary

added contributor
avoid referring to lemmas by index
documented reference
example applications of the 'metric' decision procedure, by Maximilian Schäffeler
decision procedure for metric spaces, implemented by Maximilian Schäffeler
NEWS
renamed because of duplicateion to avoid very long qualified names

Changeset 70955:73ae8c30c6cb by immler: added contributor
The file was modified	`CONTRIBUTORS` (diff)
Changeset 70954:23e6eef4e6aa by immler: avoid referring to lemmas by index
The file was modified	`src/HOL/Analysis/Metric_Arith.thy` (diff)
The file was modified	`src/HOL/Analysis/metricarith.ml` (diff)
Changeset 70953:420359ba6acd by immler: documented reference
The file was modified	`src/HOL/Analysis/Metric_Arith.thy` (diff)
The file was modified	`src/HOL/Analysis/document/root.bib` (diff)
Changeset 70952:f140135ff375 by immler: example applications of the 'metric' decision procedure, by Maximilian Schäffeler
The file was modified	`src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy` (diff)
The file was modified	`src/HOL/Analysis/Topology_Euclidean_Space.thy` (diff)
Changeset 70951:678b2abe9f7d by immler: decision procedure for metric spaces, implemented by Maximilian Schäffeler
The file was added	`src/HOL/Analysis/Metric_Arith.thy`
The file was added	`src/HOL/Analysis/metricarith.ml`
The file was modified	`src/HOL/Analysis/Elementary_Metric_Spaces.thy` (diff)
Changeset 70950:7378fa1d0892 by nipkow: NEWS
The file was modified	`NEWS` (diff)
Changeset 70949:581083959358 by nipkow: renamed because of duplicateion to avoid very long qualified names
The file was modified	`src/HOL/Complete_Lattices.thy` (diff)