3 commits

Author	SHA1	Message	Date
Leonardo de Moura	d2958044fd	feat(frontends/lean): add multiple_instances command ... After this commit, Lean "cuts" the search after the first instance is computed. To obtain the previous behavior, we must use the new command multiple_instances <class-name> closes #370	2014-12-21 17:28:44 -08:00
Jakob von Raumer	503048226e	chore(hott) fix the types and algebra	2014-12-16 13:11:32 -08:00
Jakob von Raumer	dae2aeb605	chore(hott) fix file endings	2014-12-16 13:11:32 -08:00

Renamed from hott/algebra/precategory/basic.lean (Browse further)