1signature Omega = 2sig 3 4 include Abbrev 5 val OMEGA_CONV : conv 6 val OMEGA_PROVE : conv 7 val OMEGA_TAC : tactic 8 9end 10