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 "ACL2" "MUTUAL-RECURSION") (mkpair (mkpair (mksym
22"COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "BAR") (mkpair (mkpair (mksym
23"ACL2" "X") (mksym "COMMON-LISP" "NIL")) (mkpair (mkpair (mksym "COMMON-LISP"
24"IF") (mkpair (mkpair (mksym "COMMON-LISP" "CONSP") (mkpair (mksym "ACL2" "X") (
25mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "ACL2" "BAR") (mkpair (
26mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "X") (mksym
27"COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2"
28"X") (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))) (mkpair (
29mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "H") (mkpair (
30mkpair (mksym "ACL2" "X") (mksym "COMMON-LISP" "NIL")) (mkpair (mksym "ACL2"
31"X") (mksym "COMMON-LISP" "NIL"))))) (mksym "COMMON-LISP" "NIL"))))
32
33];
34