test/Tools/isac/Knowledge/rlang.sml
changeset 48763 9b9936d79dbe
parent 42394 977788dfed26
child 52101 c3f399ce32af
     1.1 --- a/test/Tools/isac/Knowledge/rlang.sml	Sun Oct 14 14:43:41 2012 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/rlang.sml	Sun Oct 14 20:00:27 2012 +0200
     1.3 @@ -1470,13 +1470,13 @@
     1.4  ##  rls: expand on:
     1.5  ##  rls: reduce_0_1_2 on:
     1.6  ##  rls: order_add_mult on:
     1.7 -###  try thm: real_mult_commute
     1.8 +###  try thm: mult_commute
     1.9  ===  rewrites to: (a + b * x) / (a + -1 * (b * x)) + (-1 * a + -1 * (-1 * (b * x))) / (a + b * x) = b * (4 * a) / (a ^^^ 2 + -1 * b ^^^ 2)
    1.10  
    1.11  ###  try thm: real_mult_left_commute
    1.12  ===  rewrites to: (a + b * x) / (a + -1 * (b * x)) + (-1 * a + -1 * (-1 * (b * x))) / (a + b * x) = 4 * (b * a) / (a ^^^ 2 + -1 * b ^^^ 2)
    1.13  
    1.14 -###  try thm: real_mult_commute
    1.15 +###  try thm: mult_commute
    1.16  ===  rewrites to: (a + b * x) / (a + -1 * (b * x)) + (-1 * a + -1 * (-1 * (b * x))) / (a + b * x) = 4 * (a * b) / (a ^^^ 2 + -1 * b ^^^ 2)
    1.17  
    1.18  ###  try calc: op *'