defiso-doc

(in-package "ACL2")

(defxdoc defiso
  :parents (std/util defmapping)
  :short "Establish an isomorphic mapping between two domains."
  :long (topstring (p "This is a specialization of @(tsee defmapping) where
     the @(':beta-of-alpha-thm') and @(':alpha-of-beta-thm') inputs are @('t').
     See the documentation of @(tsee defmapping).")))