2 commits

Author	SHA1	Message	Date
Leonardo de Moura	b254c78c44	refactor(library/algebra): move bundled structures to separate module ... Motivation: performance. After this commit, the bundled instances do not participate in the class/instance resolution if we do not import algebra.bundled.	2015-03-02 18:45:08 -08:00
Leonardo de Moura	33e562a7ce	fix(frontends/lean/structure_cmd): effect of "include" command in the structure command ... closes #438	2015-02-19 22:44:51 -08:00