1open HolKernel Parse boolLib bossLib intSyntax pairSyntax listSyntax stringLib numLib sexp;
2
3val package =
4 implode(map chr (cons 65 (cons 67 (cons 76 (cons 50 nil)))));
5
6val events = [
7
8(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "FOO") (mkpair (
9mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL")) (mkpair (mkpair (mksym
10"COMMON-LISP" "CONS") (mkpair (mksym "ACL2" "X") (mkpair (mksym "ACL2" "X") (
11mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))))
12,
13
14(mkpair (mksym "ACL2" "DEFTHM") (mkpair (mksym "ACL2" "FOO-PROP") (mkpair (
15mkpair (mksym "COMMON-LISP" "EQUAL") (mkpair (mkpair (mksym "COMMON-LISP"
16"CAR") (mkpair (mkpair (mksym "ACL2" "FOO") (mkpair (mksym "ACL2" "X") (mksym
17"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2"
18"X") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL"))))
19,
20
21(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "BAR") (mkpair (
22mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL")) (mkpair (mkpair (mksym
23"ACL2" "FOO") (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (mksym
24"COMMON-LISP" "NIL")))))
25,
26
27(mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "H") (mkpair (
28mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL")) (mkpair (mkpair (mksym
29"ACL2" "BAR") (mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL"))) (mksym
30"COMMON-LISP" "NIL")))))
31
32];
33