Lines Matching refs:str
328 (eqlable_listp (str st) = nil)
380 (acl2_make_character_list (str st) = nil)
661 |- immediate_force_modep = str "See :DOC immediate-force-modep.",
875 (character_listp (str st) = nil)
1564 andl [symbolp x; equal (symbol_package_name x) (str KEYWORD)],
1613 ite (endp x) (str "")
1715 (str "Unexpected event-type for xd-name, %x0")
1965 (str
1971 (str
2503 str
3148 cons (asym "ACL2-VERSION") (str "ACL2 Version 2.9.3");
3153 cons (asym "CURRENT-PACKAGE") (str ACL2);
3205 cons (asym "TRIPLE-PRINT-PREFIX") (str " ");
3254 cons (asym "ACL2-VERSION") (str "ACL2 Version 2.9.3");
3259 cons (asym "CURRENT-PACKAGE") (str ACL2);
3315 cons (asym "TRIPLE-PRINT-PREFIX") (str " ");
3601 (str "Unexpected base, ~x0") print_base))
4155 (put_global (asym "CURRENT-PACKAGE") (str ACL2) state)),