(module defthm mzscheme

  (require "../private/define-below.ss")

  (provide defthm defaxiom)
  
  (define-syntax (defthm stx)
    (syntax-case stx ()
      [(_ name body hints ...)
       #'(define-below name 
           '(theorem: body))]))

  ;; To a runtime system, defthm and defaxiom are the same no-op.
  (define-syntax (defaxiom stx)
    (syntax-case stx ()
      [(_ name body hints ...) (syntax/loc stx (defthm name body hints ...))]))
  )