1344 fun normal_form t = SOME (sort_variables t,[]:term list); |
1344 fun normal_form t = SOME (sort_variables t,[]:term list); |
1345 |
1345 |
1346 val order_mult_ = |
1346 val order_mult_ = |
1347 Rrls {id = "order_mult_", |
1347 Rrls {id = "order_mult_", |
1348 prepat = |
1348 prepat = |
|
1349 (* ?p matched with the current term gives an environment, |
|
1350 which evaluates (the instantiated) "p is_multUnordered" to true*) |
1349 [([(term_of o the o (parse thy)) "p is_multUnordered"], |
1351 [([(term_of o the o (parse thy)) "p is_multUnordered"], |
1350 parse_patt thy "?p" )], |
1352 parse_patt thy "?p :: real" )], |
1351 rew_ord = ("dummy_ord", dummy_ord), |
1353 rew_ord = ("dummy_ord", dummy_ord), |
1352 erls = append_rls "e_rls-is_multUnordered" e_rls(*MG: poly_erls*) |
1354 erls = append_rls "e_rls-is_multUnordered" e_rls(*MG: poly_erls*) |
1353 [Calc ("Poly.is'_multUnordered", |
1355 [Calc ("Poly.is'_multUnordered", |
1354 eval_is_multUnordered "")], |
1356 eval_is_multUnordered "")], |
1355 calc = [("PLUS" , ("Groups.plus_class.plus" , eval_binop "#add_")), |
1357 calc = [("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_")), |
1356 ("TIMES" , ("Groups.times_class.times" , eval_binop "#mult_")), |
1358 ("TIMES" , ("Groups.times_class.times", eval_binop "#mult_")), |
1357 ("DIVIDE", ("Rings.inverse_class.divide", eval_cancel "#divide_e")), |
1359 ("DIVIDE", ("Rings.inverse_class.divide", |
|
1360 eval_cancel "#divide_e")), |
1358 ("POWER" , ("Atools.pow", eval_binop "#power_"))], |
1361 ("POWER" , ("Atools.pow", eval_binop "#power_"))], |
1359 scr=Rfuns {init_state = init_state, |
1362 scr=Rfuns {init_state = init_state, |
1360 normal_form = normal_form, |
1363 normal_form = normal_form, |
1361 locate_rule = locate_rule, |
1364 locate_rule = locate_rule, |
1362 next_rule = next_rule, |
1365 next_rule = next_rule, |