Changes

Summary

proper home directory, required for $HOME/.ssh setup;
merged
proper file name: .ML is mandatory for Isabelle/ML files;
Removed dup lemma that inhibited locale instantiations (dup fact error)
some applications of "metric"
header with Title/Author; added note on motivation of this example
a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
NEWS
added examples for "metric" method, by Maximilian Schäffeler

Changeset 70964:99eec58dc551 by wenzelm: proper home directory, required for $HOME/.ssh setup;
The file was modified	`Admin/Phabricator/README` (diff)
Changeset 70963:bbe5fe8bba71 by wenzelm: merged
Changeset 70962:e8207714d505 by wenzelm: proper file name: .ML is mandatory for Isabelle/ML files;
The file was added	`src/HOL/Analysis/metric_arith.ML`
The file was modified	`src/HOL/Analysis/Metric_Arith.thy` (diff)
The file was removed	`src/HOL/Analysis/metricarith.ml`
Changeset 70961:70fb697be418 by Peter Lammich: Removed dup lemma that inhibited locale instantiations (dup fact error)
The file was modified	`src/HOL/Library/Complete_Partial_Order2.thy` (diff)
Changeset 70960:84f79d82df0a by immler: some applications of "metric"
The file was modified	`src/HOL/Analysis/Elementary_Metric_Spaces.thy` (diff)
Changeset 70959:ba0b65d45aec by immler: header with Title/Author; added note on motivation of this example
The file was modified	`src/HOL/Eisbach/Example_Metric.thy` (diff)
Changeset 70958:e8fc52f3f175 by immler: a slower implementation of the "metric" method as Eisbach example, by Maximilian Schäffeler
The file was added	`src/HOL/Eisbach/Example_Metric.thy`
The file was modified	`src/HOL/ROOT` (diff)
Changeset 70957:aa41be39aa99 by immler: NEWS
The file was modified	`NEWS` (diff)
Changeset 70956:860198428664 by immler: added examples for "metric" method, by Maximilian Schäffeler
The file was added	`src/HOL/Analysis/ex/Metric_Arith_Examples.thy`
The file was modified	`src/HOL/ROOT` (diff)