All the core rules.
Properties of the core rules are proved in core-rules-validation.
We use add-const-to-untranslate-preprocess to keep this constant unexpanded in output.
Definition:
(defconst *core-rules* (list *rule_alpha* *rule_bit* *rule_char* *rule_cr* *rule_crlf* *rule_ctl* *rule_digit* *rule_dquote* *rule_hexdig* *rule_htab* *rule_lf* *rule_lwsp* *rule_octet* *rule_sp* *rule_vchar* *rule_wsp*))
Function:
(defun untranslate-preprocess-*core-rules* (acl2::term acl2::wrld) (if (equal acl2::term (list 'quote *core-rules*)) '*core-rules* (acl2::untranslate-preproc-for-define acl2::term acl2::wrld)))
Theorem:
(defthm rulelistp-of-*core-rules* (rulelistp *core-rules*))