ACL2-PC::CLAUSE-PROCESSOR

(atomic macro) use a clause-processor 
Major Section:  PROOF-CHECKER-COMMANDS


Example:
(cl-proc :function
	   note-fact-clause-processor
	  :hint
	  '(equal a a))
-- Invoke the indicated clause processor function with the indicated hint
argument (see the beginning of file
books/clause-processors/basic-examples.lisp.


General Form:
(cl-proc &rest cl-proc-args)
Invoke a clause-processor as indicated by cl-proc-args, which is a list of arguments that can serve as the value of a :clause-processor hint; see hints.

This command calls the prove command, and hence should only be used at the top of the conclusion.