blob: a493ab1a401666b4c341073d831728ef33412d6b (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
|
;; Example proof script for ACL2 Proof General.
;;
;; $Id$
;;
(defthm assoc->assoc-equal
(equal (assoc x a)
(assoc-equal x a)))
(defthm assoc->assoc-equal
(equal (assoc x a)
(assoc-equal x a)))
|