2 commits

Author	SHA1	Message	Date
Leonardo de Moura	9e9ebe9edd	test(tests/lean/run/even_odd): use default decreasing tactic for defining even and odd	2017-05-24 14:34:54 -07:00
Leonardo de Moura	229b730c15	feat(library/equations_compiler): invoke tactics for building well founded relation, and proving recursive calls are "decreasing"	2017-05-23 16:04:55 -07:00