7 commits

Author	SHA1	Message	Date
Rob Lewis	371638a628	fix(theories/analysis): rename derivative theorems	2016-06-02 10:45:54 -07:00
Rob Lewis	6b71b75d6f	fix(theories/move): add missing theorem to move	2016-06-02 10:45:54 -07:00
Rob Lewis	5a439942dd	feat(library/theories): adapt analysis theory to use new topological limits	2016-06-02 10:45:54 -07:00
Jeremy Avigad	b8c230a55d	refactor(library/theories/topology/approaches): rename 'filterlim' to 'tendsto' etc., and general cleaning	2016-06-02 10:45:13 -07:00
Floris van Doorn	8db4676c46	feat(hott): various changes and additions in the HoTT library ... Add more theorems about mapping cylinders, fibers, truncated 2-quotient, truncated univalence, pre/postcomposition with an iso in a precategory. renamings: equiv.refl -> equiv.rfl and equiv_eq <-> equiv_eq'	2016-05-06 14:27:27 -07:00
Jeremy Avigad	e6fd644526	feat(library/theories/group_theory/*): add new development of group theory	2016-05-06 14:15:51 -07:00
Jeremy Avigad	73271ac2c9	feat(library/theories/move.lean): add facts to move in Lean 3	2016-04-06 16:14:14 -04:00