summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--lists/perm.lisp6
1 files changed, 4 insertions, 2 deletions
diff --git a/lists/perm.lisp b/lists/perm.lisp
index 36253ec..a5b5487 100644
--- a/lists/perm.lisp
+++ b/lists/perm.lisp
@@ -58,11 +58,13 @@
(implies (and (member e x)
(not (member e y)))
(not (perm x y)))
- :hints (("Subgoal *1/3" :cases ((equal (car x) e))))))
+ :hints (("Subgoal *1/3" :cases ((equal (car x) e))))
+ :rule-classes ((:rewrite :match-free :all))))
(defthm perm-transitive
(implies (and (perm x y)
(perm y z))
- (perm x z)))))
+ (perm x z))
+ :rule-classes ((:rewrite :match-free :all)))))
(defequiv perm)