mathlib

900c53ae - feat(scripts): add scripts to import all mathlib files (#1281)

feat(scripts): add scripts to import all mathlib files (#1281) * add scripts to import all mathlib files mk_all makes a file all.lean in each subdirectory of src/, importing all files in that directory, including subdirectories rm_all removes the files all.lean * also delete all.olean files * remove unnecessary maxdepth * add comments, and generate comments