447 fun divide_cancel_numeral_factor ctxt ct = DivideCancelNumeralFactor.proc ctxt (Thm.term_of ct) |
447 fun divide_cancel_numeral_factor ctxt ct = DivideCancelNumeralFactor.proc ctxt (Thm.term_of ct) |
448 |
448 |
449 val field_divide_cancel_numeral_factor = |
449 val field_divide_cancel_numeral_factor = |
450 [prep_simproc @{theory} |
450 [prep_simproc @{theory} |
451 ("field_divide_cancel_numeral_factor", |
451 ("field_divide_cancel_numeral_factor", |
452 ["((l::'a::field_inverse_zero) * m) / n", |
452 ["((l::'a::field) * m) / n", |
453 "(l::'a::field_inverse_zero) / (m * n)", |
453 "(l::'a::field) / (m * n)", |
454 "((numeral v)::'a::field_inverse_zero) / (numeral w)", |
454 "((numeral v)::'a::field) / (numeral w)", |
455 "((numeral v)::'a::field_inverse_zero) / (- numeral w)", |
455 "((numeral v)::'a::field) / (- numeral w)", |
456 "((- numeral v)::'a::field_inverse_zero) / (numeral w)", |
456 "((- numeral v)::'a::field) / (numeral w)", |
457 "((- numeral v)::'a::field_inverse_zero) / (- numeral w)"], |
457 "((- numeral v)::'a::field) / (- numeral w)"], |
458 DivideCancelNumeralFactor.proc)]; |
458 DivideCancelNumeralFactor.proc)]; |
459 |
459 |
460 val field_cancel_numeral_factors = |
460 val field_cancel_numeral_factors = |
461 prep_simproc @{theory} |
461 prep_simproc @{theory} |
462 ("field_eq_cancel_numeral_factor", |
462 ("field_eq_cancel_numeral_factor", |