Skip to content
Success

Changes

Summary

  1. fixes esp to theory presentation
  2. new material ported from HOL Light's metric.ml
Changeset 77942:30f69046f120 by paulson _lp15@cam.ac.uk_:
fixes esp to theory presentation
The file was modified src/HOL/Analysis/Abstract_Topological_Spaces.thy (diff)
Changeset 77941:c35f06b0931e by paulson _lp15@cam.ac.uk_:
new material ported from HOL Light's metric.ml
The file was addedsrc/HOL/Analysis/Abstract_Topological_Spaces.thy
The file was modified src/HOL/Analysis/Analysis.thy (diff)