2 commits

Author	SHA1	Message	Date
Sebastian Ullrich	77c20e99ff	feat(library/tactic/inversion_tactic): consistent orientation of generated equalities ... Generated equalities in proof irrelevant environments were inverted compared with the documentation and the proof relevant case, which resulted in newly generated local vars replacing equivalent old ones instead of the other way around.	2015-05-14 23:32:54 +02:00
Leonardo de Moura	326048df54	feat(library/tactic/inversion_tactic): clear variables that have been eliminated by cases tactic ... see discussion at: https://groups.google.com/forum/#!topic/lean-discuss/oyzgIqdMyNc	2015-05-02 19:33:59 -07:00