[isabelle-dev] Redundant definitions in Analysis
sebastien.gouezel at univ-nantes.fr
Mon Mar 11 20:27:50 CET 2019
Le 11/03/2019 à 19:13, Fabian Immler a écrit :
> Sébastien might have a stronger opinion (I don't), but I would also go
> for continuous_map: it is in line with open_map, closed_map,
> quotient_map (which we don't have as constants, but use in theorem
> names). Moreover, we have more occurrences of continuous_map (174+0 vs
> 83+39 in isabelle+AFP).
You can definitely go for continuous_map.
More information about the isabelle-dev