Commit 441bd264 authored by Heiko Becker's avatar Heiko Becker
Browse files

Make split stronger, resp. behave like the coq split

parent f0a320f9
......@@ -39,7 +39,9 @@ let lcontra asm ty = lcontradiction asm ty;;
let destruct (asm:string) (patt:string) =
REMOVE_THEN asm (DESTRUCT_TAC patt);;
let split = CONJ_TAC;;
let split = if (is_conj (snd (top_goal()))) then CONJ_TAC
else if (is_eq (snd (top_goal()))) then EQ_TAC
else failwith "No destructable equivalence found";;
let left = DISJ1_TAC;;
let right = DISJ2_TAC;;
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment