RING_AND_IDEAL_CONV : (term -> num) * (num -> term) * conv * term * term * term * term * term * term * term * thm * (term -> thm) -> (term -> thm) * (term list -> term -> term list)
Returns a pair giving a ring proof procedure and an ideal membership routine.
This function combines the functionality of RING and ideal_cofactors. Each
of these requires the same rather lengthy input. When you want to apply both to
the same set of parameters, you can do so using RING_AND_IDEAL_CONV. That is:
is functionally equivalent to:
For more information, see the documentation for those two functions.
RING parms,ideal_cofactors parms
- FAILURE CONDITIONS
Fails if the parameters are wrong.
- SEE ALSO