321 term_ord' 1 pr x thy (TermC.numerals_to_Free ts, TermC.numerals_to_Free us) = LESS |
321 term_ord' 1 pr x thy (TermC.numerals_to_Free ts, TermC.numerals_to_Free us) = LESS |
322 | _ => raise ERROR ("ord_make_polynomial_in called with subst = " ^ Env.subst2str subst)) |
322 | _ => raise ERROR ("ord_make_polynomial_in called with subst = " ^ Env.subst2str subst)) |
323 |
323 |
324 (** )end;( *local*) |
324 (** )end;( *local*) |
325 |
325 |
326 val subs = [(TermC.str2term "bdv::real", TermC.str2term "x::real")]; |
326 val subs = [(TermC.parse_test @{context} "bdv::real", TermC.parse_test @{context} "x::real")]; |
327 if ord_make_polynomial_in false(*true*) @{theory} subs (t1, t2) then () else error "still GREATER?"; |
327 if ord_make_polynomial_in false(*true*) @{theory} subs (t1, t2) then () else error "still GREATER?"; |
328 |
328 |
329 val x = TermC.str2term "x ::real"; |
329 val x = TermC.parse_test @{context} "x ::real"; |
330 |
330 |
331 val t1 = TermC.numerals_to_Free (TermC.str2term "L * q_0 * x \<up> 2 / 4 ::real"); |
331 val t1 = TermC.numerals_to_Free (TermC.parse_test @{context} "L * q_0 * x \<up> 2 / 4 ::real"); |
332 if 2006 = size_of_term' 1 false(*true*) x t1 |
332 if 2006 = size_of_term' 1 false(*true*) x t1 |
333 then () else error "size_of_term' (L * q_0 * x \<up> 2) CHANGED)"; |
333 then () else error "size_of_term' (L * q_0 * x \<up> 2) CHANGED)"; |
334 |
334 |
335 val t2 = TermC.numerals_to_Free (TermC.str2term "- 1 * (q_0 * x \<up> 3) :: real"); |
335 val t2 = TermC.numerals_to_Free (TermC.parse_test @{context} "- 1 * (q_0 * x \<up> 3) :: real"); |
336 if 3004 = size_of_term' 1 false(*true*) x t2 |
336 if 3004 = size_of_term' 1 false(*true*) x t2 |
337 then () else error "size_of_term' (- 1 * (q_0 * x \<up> 3)) CHANGED"; |
337 then () else error "size_of_term' (- 1 * (q_0 * x \<up> 3)) CHANGED"; |
338 |
338 |
339 |
339 |
340 "----------- Matthias Goldgruber 2003 trials on rewrite orders -------------------------------"; |
340 "----------- Matthias Goldgruber 2003 trials on rewrite orders -------------------------------"; |