src/Tools/isac/Knowledge/LinEq.thy
changeset 59637 8881c5d28f82
parent 59635 9fc1bb69813c
child 59773 d88bb023c380
     1.1 --- a/src/Tools/isac/Knowledge/LinEq.thy	Wed Oct 02 15:14:51 2019 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/LinEq.thy	Wed Oct 02 16:02:17 2019 +0200
     1.3 @@ -140,13 +140,13 @@
     1.4  "solve_linear_equation e_e v_v = (
     1.5    let
     1.6      e_e = (
     1.7 -      (Try (Rewrite ''all_left'')) @@
     1.8 -      (Try (Repeat (Rewrite ''makex1_x''))) @@
     1.9 -      (Try (Rewrite_Set ''expand_binoms'')) @@
    1.10 -      (Try (Repeat (Rewrite_Set_Inst [(''bdv'', v_v)] ''make_ratpoly_in''))) @@
    1.11 +      (Try (Rewrite ''all_left'')) #>
    1.12 +      (Try (Repeat (Rewrite ''makex1_x''))) #>
    1.13 +      (Try (Rewrite_Set ''expand_binoms'')) #>
    1.14 +      (Try (Repeat (Rewrite_Set_Inst [(''bdv'', v_v)] ''make_ratpoly_in''))) #>
    1.15        (Try (Repeat (Rewrite_Set ''LinPoly_simplify''))) ) e_e;
    1.16      e_e = (
    1.17 -      (Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''LinEq_simplify'')) @@
    1.18 +      (Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''LinEq_simplify'')) #>
    1.19        (Repeat (Try (Rewrite_Set ''LinPoly_simplify''))) ) e_e
    1.20    in
    1.21      Or_to_List e_e)"