Mercurial > cpdt > repo

comparison src/Tactics.v @ 38:95e24b629ad9

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Exercises
author Adam Chlipala <adamc@hcoop.net>
date Fri, 12 Sep 2008 16:55:37 -0400
parents 6d05ee182b65
children a21eb02cc7c6
comparison
equal deleted inserted replaced
37:c9ade53b27aa 38:95e24b629ad9
6 * The license text is available at: 6 * The license text is available at:
7 * http://creativecommons.org/licenses/by-nc-nd/3.0/ 7 * http://creativecommons.org/licenses/by-nc-nd/3.0/
8 *) 8 *)
9 9
10 Require Import List. 10 Require Import List.
11
12 Require Omega.
11 13
12 14
13 Ltac rewriteHyp := 15 Ltac rewriteHyp :=
14 match goal with 16 match goal with
15 | [ H : _ |- _ ] => rewrite H 17 | [ H : _ |- _ ] => rewrite H
21 23
22 Hint Rewrite app_ass : cpdt. 24 Hint Rewrite app_ass : cpdt.
23 25
24 Ltac sintuition := simpl in *; intuition. 26 Ltac sintuition := simpl in *; intuition.
25 27
26 Ltac crush := sintuition; rewriter; sintuition. 28 Ltac crush := sintuition; rewriter; sintuition; try omega.