Mercurial > cpdt > repo

comparison src/Tactics.v @ 80:506a06118014

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Try arithmetic contradiction
author Adam Chlipala <adamc@hcoop.net>
date Sat, 04 Oct 2008 14:58:00 -0400
parents b52204928c7d
children 522436ed6688
comparison
equal deleted inserted replaced
79:6c2607211cee 80:506a06118014
110 Ltac crush' lemmas invOne := 110 Ltac crush' lemmas invOne :=
111 let sintuition := simpl in *; intuition; try subst; repeat (simplHyp invOne; intuition; try subst); try congruence 111 let sintuition := simpl in *; intuition; try subst; repeat (simplHyp invOne; intuition; try subst); try congruence
112 in (sintuition; rewriter; 112 in (sintuition; rewriter;
113 repeat ((app ltac:(fun L => inster L L) lemmas || appHyps ltac:(fun L => inster L L)); 113 repeat ((app ltac:(fun L => inster L L) lemmas || appHyps ltac:(fun L => inster L L));
114 repeat (simplHyp invOne; intuition)); 114 repeat (simplHyp invOne; intuition));
115 un_done; sintuition; try omega). 115 un_done; sintuition; try omega; try (elimtype False; omega)).
116 116
117 Ltac crush := crush' tt fail. 117 Ltac crush := crush' tt fail.