4 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
Leonardo de Moura	d9d822baa7	feat(library/tactic/class_instance_synth): add mk_hset_instance procedure	2014-12-19 22:00:25 -08:00
Leonardo de Moura	d6f79423e9	feat(library/tactic/class_instance_synth): add mk_class_instance procedures	2014-12-19 20:09:09 -08:00
Leonardo de Moura	4421069e34	refactor(library/tactic): rename placeholder_elaborator to class_instance_synth	2014-12-19 19:57:38 -08:00

Renamed from src/library/tactic/placeholder_elaborator.cpp (Browse further)