aboutsummaryrefslogtreecommitdiffhomepage
path: root/acl2/example.acl2
diff options
context:
space:
mode:
Diffstat (limited to 'acl2/example.acl2')
-rw-r--r--acl2/example.acl24
1 files changed, 0 insertions, 4 deletions
diff --git a/acl2/example.acl2 b/acl2/example.acl2
index a493ab1a..a3a0f211 100644
--- a/acl2/example.acl2
+++ b/acl2/example.acl2
@@ -7,7 +7,3 @@
(equal (assoc x a)
(assoc-equal x a)))
-(defthm assoc->assoc-equal
- (equal (assoc x a)
- (assoc-equal x a)))
-