classes

(in-package "ACL2")

(define classes
  ((thm symbolp) (wrld plist-worldp))
  :returns (classes "A @(tsee keyword-to-keyword-value-list-alistp).")
  :parents (std/system/theorem-queries)
  :short "Rule classes of a theorem."
  :long (topstring (p "See @(tsee classes+) for an enhanced variant of this utility."))
  (getpropc thm 'classes nil wrld))