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