File: example.acl2

package info (click to toggle)
proofgeneral 4.2~pre120605-2
  • links: PTS
  • area: main
  • in suites: wheezy
  • size: 5,060 kB
  • sloc: lisp: 35,277; ml: 2,239; sh: 288; makefile: 250; perl: 159
file content (9 lines) | stat: -rw-r--r-- 190 bytes parent folder | download 
1
2
3
4
5
6
7
8
9
 
;;  Example proof script for ACL2 Proof General.
;;
;;   $Id: example.acl2,v 12.0 2011/10/13 10:54:47 da Exp $
;;    

(defthm assoc->assoc-equal
  (equal (assoc x a)
	 (assoc-equal x a)))