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)"