Searched +refs:M1 +refs:MAKE +refs:DEFUN (Results 1 - 6 of 6) sorted by relevance

/seL4-l4v-10.1.1/HOL4/examples/acl2/examples/M1/
H A Dm1_story.sml8 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "NEXT-INST") (
9 mkpair (mkpair (mksym "M1" "S") (mksym "COMMON-LISP" "NIL")) (mkpair (mkpair (
10 mksym "M1" "NTH") (mkpair (mkpair (mksym "M1" "PC") (mkpair (mksym "M1" "S") (
11 mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "PROGRAM") (mkpair (
12 mksym "M1" "S") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (
16 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "EXECUT
[all...]
H A Dproblem_set_1_answers.sml8 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "PUSH") (mkpair (
9 mkpair (mksym "M1" "X") (mkpair (mksym "M1" "Y") (mksym "COMMON-LISP" "NIL"))) (
10 mkpair (mkpair (mksym "COMMON-LISP" "CONS") (mkpair (mksym "M1" "X") (mkpair (
11 mksym "M1" "Y") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))))
14 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "TOP") (mkpair (
15 mkpair (mksym "M1" "STACK") (mksym "COMMON-LISP" "NIL")) (mkpair (mkpair (
16 mksym "COMMON-LISP" "CAR") (mkpair (mksym "M1" "STAC
[all...]
H A DPKGS.sml326 ("DEFUN" , "ACL2" , "COMMON-LISP"),
586 ("MAKE-ARRAY" , "ACL2" , "COMMON-LISP"),
588 ("MAKE-BROADCAST-STREAM" , "ACL2" , "COMMON-LISP"),
590 ("MAKE-CONCATENATED-STREAM" , "ACL2" , "COMMON-LISP"),
592 ("MAKE-CONDITION" , "ACL2" , "COMMON-LISP"),
594 ("MAKE-DISPATCH-MACRO-CHARACTER" , "ACL2" , "COMMON-LISP"),
596 ("MAKE-ECHO-STREAM" , "ACL2" , "COMMON-LISP"),
598 ("MAKE-HASH-TABLE" , "ACL2" , "COMMON-LISP"),
600 ("MAKE-INSTANCE" , "ACL2" , "COMMON-LISP"),
602 ("MAKE
[all...]
/seL4-l4v-10.1.1/HOL4/examples/acl2/tests/gold/
H A Dm1_story.sml8 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "NEXT-INST") (
9 mkpair (mkpair (mksym "M1" "S") (mksym "COMMON-LISP" "NIL")) (mkpair (mkpair (
10 mksym "M1" "NTH") (mkpair (mkpair (mksym "M1" "PC") (mkpair (mksym "M1" "S") (
11 mksym "COMMON-LISP" "NIL"))) (mkpair (mkpair (mksym "M1" "PROGRAM") (mkpair (
12 mksym "M1" "S") (mksym "COMMON-LISP" "NIL"))) (mksym "COMMON-LISP" "NIL")))) (
16 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "EXECUT
[all...]
H A Dproblem_set_1_answers.sml8 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "PUSH") (mkpair (
9 mkpair (mksym "M1" "X") (mkpair (mksym "M1" "Y") (mksym "COMMON-LISP" "NIL"))) (
10 mkpair (mkpair (mksym "COMMON-LISP" "CONS") (mkpair (mksym "M1" "X") (mkpair (
11 mksym "M1" "Y") (mksym "COMMON-LISP" "NIL")))) (mksym "COMMON-LISP" "NIL")))))
14 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "TOP") (mkpair (
15 mkpair (mksym "M1" "STACK") (mksym "COMMON-LISP" "NIL")) (mkpair (mkpair (
16 mksym "COMMON-LISP" "CAR") (mkpair (mksym "M1" "STAC
[all...]
/seL4-l4v-10.1.1/HOL4/examples/acl2/tests/inputs/
H A DPKGS.sml285 ("DEFUN" , "ACL2" , "COMMON-LISP"),
545 ("MAKE-ARRAY" , "ACL2" , "COMMON-LISP"),
547 ("MAKE-BROADCAST-STREAM" , "ACL2" , "COMMON-LISP"),
549 ("MAKE-CONCATENATED-STREAM" , "ACL2" , "COMMON-LISP"),
551 ("MAKE-CONDITION" , "ACL2" , "COMMON-LISP"),
553 ("MAKE-DISPATCH-MACRO-CHARACTER" , "ACL2" , "COMMON-LISP"),
555 ("MAKE-ECHO-STREAM" , "ACL2" , "COMMON-LISP"),
557 ("MAKE-HASH-TABLE" , "ACL2" , "COMMON-LISP"),
559 ("MAKE-INSTANCE" , "ACL2" , "COMMON-LISP"),
561 ("MAKE
[all...]

Completed in 103 milliseconds