Searched +refs:M1 +refs:NTH +refs:UPDATE +refs:NTH (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" "EXECUTE-ICONST") (
17 mkpair (mkpair (mksym "M1" "INS
[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" "STACK") (mksym "COMMON-LISP"
20 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "POP") (mkpair (
21 mkpair (mksym "M1" "STAC
[all...]
H A DPKGS.sml696 ("NTH" , "ACL2" , "COMMON-LISP"),
698 ("NTH-VALUE" , "ACL2" , "COMMON-LISP"),
1004 ("UPDATE-INSTANCE-FOR-DIFFERENT-CLASS" , "ACL2" , "COMMON-LISP"),
1006 ("UPDATE-INSTANCE-FOR-REDEFINED-CLASS" , "ACL2" , "COMMON-LISP"),
1133 ("ADD-NTH-ALIAS" , "ACL2-USER" , "ACL2"),
1375 ("CHARACTERP-NTH" , "ACL2-USER" , "ACL2"),
1916 ("LEN-UPDATE-NTH" , "ACL2-USER" , "ACL2"),
2076 ("MV-NTH" , "ACL2-USER" , "ACL2"),
2116 ("NTH" , "ACL
[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" "EXECUTE-ICONST") (
17 mkpair (mkpair (mksym "M1" "INS
[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" "STACK") (mksym "COMMON-LISP"
20 (mkpair (mksym "COMMON-LISP" "DEFUN") (mkpair (mksym "M1" "POP") (mkpair (
21 mkpair (mksym "M1" "STAC
[all...]
/seL4-l4v-10.1.1/HOL4/examples/acl2/tests/inputs/
H A DPKGS.sml655 ("NTH" , "ACL2" , "COMMON-LISP"),
657 ("NTH-VALUE" , "ACL2" , "COMMON-LISP"),
963 ("UPDATE-INSTANCE-FOR-DIFFERENT-CLASS" , "ACL2" , "COMMON-LISP"),
965 ("UPDATE-INSTANCE-FOR-REDEFINED-CLASS" , "ACL2" , "COMMON-LISP"),
1092 ("ADD-NTH-ALIAS" , "ACL2-USER" , "ACL2"),
1334 ("CHARACTERP-NTH" , "ACL2-USER" , "ACL2"),
1875 ("LEN-UPDATE-NTH" , "ACL2-USER" , "ACL2"),
2035 ("MV-NTH" , "ACL2-USER" , "ACL2"),
2075 ("NTH" , "ACL
[all...]

Completed in 144 milliseconds