2 commits

Author	SHA1	Message	Date
Leonardo de Moura	6bc89f0916	feat(library/definitional): define ibelow and below ... These are helper definitions for brec_on and binduction_on	2014-11-12 16:38:46 -08:00
Leonardo de Moura	a3066e3eaa	fix(frontends/lean/inductive_cmd): bug in inductive datatype elaborator	2014-11-12 13:10:19 -08:00