e379034b95
- It uses the unifier in "conservative" mode - It only affects the current goal closes #570
12 lines
287 B
Text
12 lines
287 B
Text
import logic
|
||
open tactic
|
||
|
||
theorem tst (a b : Prop) (H : ¬ a ∨ ¬ b) (Hb : b) : ¬ a ∧ b
|
||
:= begin
|
||
apply and.intro,
|
||
exact
|
||
(assume Ha, or.elim H
|
||
(assume Hna, @absurd _ false Ha Hna)
|
||
(assume Hnb, @absurd _ false Hb Hnb)),
|
||
assumption
|
||
end
|