FC: suppress _aux suffixes of (used) definitions, add prime suffix to...
FC: suppress _aux suffixes of (used) definitions, add prime suffix to corresponding unsuffixed (unused) lemmas.
Showing
- Lebesgue/bochner_integral/BInt_Bif.v 4 additions, 4 deletionsLebesgue/bochner_integral/BInt_Bif.v
- Lebesgue/bochner_integral/BInt_LInt_p.v 3 additions, 3 deletionsLebesgue/bochner_integral/BInt_LInt_p.v
- Lebesgue/bochner_integral/BInt_sf.v 11 additions, 11 deletionsLebesgue/bochner_integral/BInt_sf.v
- Lebesgue/bochner_integral/Bi_fun.v 1 addition, 1 deletionLebesgue/bochner_integral/Bi_fun.v
- Lebesgue/bochner_integral/simpl_fun.v 28 additions, 28 deletionsLebesgue/bochner_integral/simpl_fun.v
Loading
Please register or sign in to comment