[isabelle-dev] Redundant definitions in Analysis

Sebastien Gouezel 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 mailing list