File: test-fix-cert0.lisp

package info (click to toggle)
acl2 4.3-3
  • links: PTS
  • area: main
  • in suites: wheezy
  • size: 76,444 kB
  • sloc: lisp: 951,371; makefile: 3,491; sh: 1,669; perl: 1,639; ansic: 358; cpp: 245; csh: 125; haskell: 17; java: 12
file content (15 lines) | stat: -rw-r--r-- 368 bytes parent folder | download | duplicates (2)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
(in-package "ACL2")

(include-book "fix-cert")

(defttag :test-fix-cert)

(progn!
 ;(trace$ fix-cert-fn)     ; for debugging
 ;(trace$ parse-book-name) ; for debugging
 (fix-cert ("moved/test1bb" "moved/test1bp"))
 (fix-cert '("moved/test1pp" "moved/test1pb"))
 (fix-cert "moved/test1b")
 (fix-cert "moved/test1p")
 (fix-cert "moved/test1")
 (fix-cert "moved/test2"))