« first day (1131 days earlier)   

SK19
SK19
19:40
@SophieSwett I think Mizar does that. You get the func definitions included as notations and constructors and if you want to refer to the definiens you have to reference the definitional theorem

« first day (1131 days earlier)