1.1 --- a/src/Tools/isac/Knowledge/LinEq.thy	Thu Sep 26 17:47:10 2019 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/LinEq.thy	Tue Oct 01 10:47:25 2019 +0200
     1.3 @@ -137,17 +137,19 @@
     1.4  
     1.5  partial_function (tailrec) solve_linear_equation :: "bool \<Rightarrow> real \<Rightarrow> bool list"
     1.6    where
     1.7 -"solve_linear_equation e_e v_v =
     1.8 -(let e_e =((Try         (Rewrite     ''all_left''            False)) @@
     1.9 -           (Try (Repeat (Rewrite     ''makex1_x''            False))) @@
    1.10 -           (Try         (Rewrite_Set ''expand_binoms''       False)) @@
    1.11 -           (Try (Repeat (Rewrite_Set_Inst [(''bdv'', v_v)]
    1.12 -                                     ''make_ratpoly_in''     False))) @@
    1.13 -           (Try (Repeat (Rewrite_Set ''LinPoly_simplify''    False))))e_e;
    1.14 -     e_e = ((Try (Rewrite_Set_Inst [(''bdv'', v_v::real)]
    1.15 -                                     ''LinEq_simplify'' True)) @@
    1.16 -            (Repeat(Try (Rewrite_Set ''LinPoly_simplify''    False)))) e_e
    1.17 - in Or_to_List e_e)"
    1.18 +"solve_linear_equation e_e v_v = (
    1.19 +  let
    1.20 +    e_e = (
    1.21 +      (Try (Rewrite ''all_left'')) @@
    1.22 +      (Try (Repeat (Rewrite ''makex1_x''))) @@
    1.23 +      (Try (Rewrite_Set ''expand_binoms'')) @@
    1.24 +      (Try (Repeat (Rewrite_Set_Inst [(''bdv'', v_v)] ''make_ratpoly_in''))) @@
    1.25 +      (Try (Repeat (Rewrite_Set ''LinPoly_simplify''))) ) e_e;
    1.26 +    e_e = (
    1.27 +      (Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''LinEq_simplify'')) @@
    1.28 +      (Repeat (Try (Rewrite_Set ''LinPoly_simplify''))) ) e_e
    1.29 +  in
    1.30 +    Or_to_List e_e)"
    1.31  setup \<open>KEStore_Elems.add_mets
    1.32      [Specify.prep_met thy "met_eq_lin" [] Celem.e_metID
    1.33        (["LinEq","solve_lineq_equation"],