1structure Omega :> Omega =
2struct
3
4 open HolKernel boolLib OmegaShell IntDP_Munge
5
6 val OMEGA_CONV = BASIC_CONV "OMEGA_CONV" decide_closed_presburger
7
8 val OMEGA_PROVE = EQT_ELIM o OMEGA_CONV
9 val OMEGA_TAC = conv_tac OMEGA_CONV
10
11end;
12