banner

(in-package "ACL2")

(make-event (prog2$ (observation-cw 'non-linear-arithmetic
      "To turn on non-linear arithmetic, execute :~|~%~Y02~|~%~
    or :~|~%~Y12~|~%~
    See the README for more about non-linear arithmetic and ~
    general information about using this library."
      '(set-default-hints '((nonlinearp-default-hint stable-under-simplificationp
           hist
           pspv)))
      '(set-default-hints '((nonlinearp-default-hint++ id
           stable-under-simplificationp
           hist
           nil)))
      nil)
    '(value-triple nil))
  :check-expansion t)