		Search-engine friendly clone of the ACL2 documentation.

Keywords

restricted-jkeywords

The restricted Java keywords, as ACL2 strings.

Definition: *restricted-jkeywords*

(defconst *restricted-jkeywords*
  (list "open" "module"
        "requires" "transitive" "exports"
        "opens" "to" "uses" "provides" "with"))

Definitions and Theorems

Theorem: ascii-listp-of-*restricted-jkeywords*

(defthm ascii-listp-of-*restricted-jkeywords*
  (implies (member-equal keyword *restricted-jkeywords*)
           (ascii-listp (string=>unicode keyword))))