equal
deleted
inserted
replaced
373 end; |
373 end; |
374 |
374 |
375 local |
375 local |
376 val rawrule = fconv_rule (arg_conv (rewr_conv @{thm real_eq_0_iff_le_ge_0})) |
376 val rawrule = fconv_rule (arg_conv (rewr_conv @{thm real_eq_0_iff_le_ge_0})) |
377 fun conj_pair th = (th RS @{thm conjunct1}, th RS @{thm conjunct2}) |
377 fun conj_pair th = (th RS @{thm conjunct1}, th RS @{thm conjunct2}) |
378 fun simple_cterm_ord t u = Term_Ord.term_ord (Thm.term_of t, Thm.term_of u) = LESS; |
378 fun simple_cterm_ord t u = Thm.term_ord (t, u) = LESS; |
379 (* FIXME: Lookup in the context every time!!! Fix this !!!*) |
379 (* FIXME: Lookup in the context every time!!! Fix this !!!*) |
380 fun splitequation ctxt th acc = |
380 fun splitequation ctxt th acc = |
381 let |
381 let |
382 val real_poly_neg_conv = #neg |
382 val real_poly_neg_conv = #neg |
383 (Semiring_Normalizer.semiring_normalizers_ord_wrapper ctxt |
383 (Semiring_Normalizer.semiring_normalizers_ord_wrapper ctxt |