acl2/ml/defaxioms.lisp.trans.ml

5084 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "ACL2" "BIG-CLOCK-ENTRY") (
5093 "UPDATE-BIG-CLOCK-ENTRY") (mkpair (mkpair (mksym "ACL2" "X") (mkpair (mksym
5884 "COMMON-LISP" "INTEGERP") (mkpair (mkpair (mksym "ACL2" "BIG-CLOCK-ENTRY") (
7001 mkpair (mksym "COMMON-LISP" "LAMBDA") (mkpair (mkpair (mksym "ACL2" "ENTRY") (
7007 mksym "ACL2" "ENTRY") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
7009 "COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "ENTRY") (mksym "COMMON-LISP"
7026 mkpair (mksym "COMMON-LISP" "LAMBDA") (mkpair (mkpair (mksym "ACL2" "ENTRY") (
7032 mksym "ACL2" "ENTRY") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
7034 "COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "ENTRY") (mksym "COMMON-LISP"
7172 "LAMBDA") (mkpair (mkpair (mksym "ACL2" "ENTRY") (mkpair (mksym "ACL2"
7176 mksym "ACL2" "ENTRY") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP"
7180 mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "ENTRY") (
7182 mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "ENTRY") (
7201 "LAMBDA") (mkpair (mkpair (mksym "ACL2" "ENTRY") (mksym "COMMON-LISP" "NIL")) (
7203 "COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "ENTRY") (mksym "COMMON-LISP"
7215 "LAMBDA") (mkpair (mkpair (mksym "ACL2" "ENTRY") (mkpair (mksym "ACL2"
7219 mksym "ACL2" "ENTRY") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP"
7223 mkpair (mkpair (mksym "COMMON-LISP" "CAR") (mkpair (mksym "ACL2" "ENTRY") (
7225 mkpair (mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "ENTRY") (
7244 "LAMBDA") (mkpair (mkpair (mksym "ACL2" "ENTRY") (mkpair (mksym "ACL2"
7247 "COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "ENTRY") (mksym "COMMON-LISP"
7252 mkpair (mksym "ACL2" "ENTRY") (mksym "COMMON-LISP" "NIL"))) (mksym
7257 mksym "ACL2" "ENTRY") (mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym
7259 mksym "ACL2" "ENTRY") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP"
7588 mkpair (mksym "ACL2" "BIG-CLOCK-ENTRY") (mkpair (mksym "ACL2" "STATE-STATE") (
7596 "COMMON-LISP" "NIL")) (mkpair (mkpair (mksym "ACL2" "UPDATE-BIG-CLOCK-ENTRY") (
7599 mkpair (mkpair (mksym "ACL2" "BIG-CLOCK-ENTRY") (mkpair (mksym "ACL2"
7967 "ENTRY") (mksym "COMMON-LISP" "NIL")) (mkpair (mkpair (mksym "COMMON-LISP"
7970 mkpair (mksym "COMMON-LISP" "CDR") (mkpair (mksym "ACL2" "ENTRY") (mksym
7972 "NIL"))) (mksym "COMMON-LISP" "NIL"))) (mkpair (mksym "ACL2" "ENTRY") (mkpair (