|
|
|---|
|
|
|
|---|
(atomic macro) prove using an existing theorem
Example: (by car-cons (x (append a b)) (y nil)) ;; This will attempt to prove the current goal by applying ;; the theorem car-cons with the given substitution. General Form: (by thm-name subst1 ... substk)
Under the hood, this command simply calls ACL2-pc::prove
with the appropriate