ordinals-without-arithmetic

Included Books

limits

other

(in-package "ACL2")

include-book

(include-book "limits")

in-theory

(in-theory (disable o< o+ o- o* o^))