Changes

Summary

introduced class topological_group between topological_monoid and real_normed_vector

Changeset 63081:5a5beb3dbe7e by immler: introduced class topological_group between topological_monoid and real_normed_vector
The file was modified	`src/HOL/Limits.thy` (diff)