other
(in-package "OBAG")
other
(include-book "core")
other
(include-book "centaur/fty/top" :dir :system)
other
(defsection emptyp-fix
:extension emptyp
(deffixequiv emptyp))
other
(defsection head-fix
:extension head
(deffixequiv head))
other
(defsection tail-fix
:extension tail
(deffixequiv tail))
other
(defsection insert-fix :extension insert (deffixequiv insert :hints (("Goal" :in-theory (enable insert)))))
other
(defsection delete-fix :extension delete (deffixequiv delete :hints (("Goal" :in-theory (enable delete)))))
other
(defsection in-fix :extension in (deffixequiv in :hints (("Goal" :in-theory (enable in)))))
other
(defsection occs-fix :extension occs (deffixequiv occs :hints (("Goal" :in-theory (enable occs)))))
other
(defsection cardinality-fix :extension cardinality (deffixequiv cardinality :hints (("Goal" :in-theory (enable cardinality)))))
other
(defsection subfix :extension subbag (deffixequiv subbag :hints (("Goal" :in-theory (enable subbag)))))
other
(defsection union-fix :extension union (deffixequiv union :hints (("Goal" :in-theory (enable union)))))
other
(defsection intersect-fix :extension intersect (deffixequiv intersect :hints (("Goal" :in-theory (enable intersect)))))
other
(defsection difference-fix :extension difference (deffixequiv difference :hints (("Goal" :in-theory (enable difference)))))