signature Omega = sig include Abbrev val OMEGA_CONV : conv val OMEGA_PROVE : conv val OMEGA_TAC : tactic end
HOL 4, Kananaskis-13