equal
deleted
inserted
replaced
749 val {add,mul,neg,pow,sub,main} = |
749 val {add,mul,neg,pow,sub,main} = |
750 Normalizer.semiring_normalizers_ord_wrapper ctxt |
750 Normalizer.semiring_normalizers_ord_wrapper ctxt |
751 (the (Normalizer.match ctxt @{cterm "(0::real) + 1"})) |
751 (the (Normalizer.match ctxt @{cterm "(0::real) + 1"})) |
752 simple_cterm_ord |
752 simple_cterm_ord |
753 in gen_real_arith ctxt |
753 in gen_real_arith ctxt |
754 (cterm_of_rat, field_comp_conv, field_comp_conv,field_comp_conv, |
754 (cterm_of_rat, Normalizer.field_comp_conv, Normalizer.field_comp_conv, Normalizer.field_comp_conv, |
755 main,neg,add,mul, prover) |
755 main,neg,add,mul, prover) |
756 end; |
756 end; |
757 |
757 |
758 end |
758 end |