1.1 --- a/src/Tools/isac/Knowledge/LinEq.thy	Fri Feb 15 16:52:05 2019 +0100
     1.2 +++ b/src/Tools/isac/Knowledge/LinEq.thy	Tue Feb 19 19:35:12 2019 +0100
     1.3 @@ -140,6 +140,19 @@
     1.4          "empty_script")]
     1.5  \<close>
     1.6      (* ansprechen mit ["LinEq","solve_univar_equation"] *)
     1.7 +partial_function (tailrec) solve_linear_equation :: "bool \<Rightarrow> real \<Rightarrow> bool list"
     1.8 +  where
     1.9 +"solve_linear_equation e_e v_v =
    1.10 +(let e_e =((Try         (Rewrite     ''all_left''            False)) @@
    1.11 +           (Try (Repeat (Rewrite     ''makex1_x''            False))) @@
    1.12 +           (Try         (Rewrite_Set ''expand_binoms''       False)) @@
    1.13 +           (Try (Repeat (Rewrite_Set_Inst [(''bdv'', v_v)]
    1.14 +                                     ''make_ratpoly_in''     False))) @@
    1.15 +           (Try (Repeat (Rewrite_Set ''LinPoly_simplify''    False))))e_e;
    1.16 +     e_e = ((Try (Rewrite_Set_Inst [(''bdv'', v_v::real)]
    1.17 +                                     ''LinEq_simplify'' True)) @@
    1.18 +            (Repeat(Try (Rewrite_Set ''LinPoly_simplify''    False)))) e_e
    1.19 + in Or_to_List e_e)"
    1.20  setup \<open>KEStore_Elems.add_mets
    1.21      [Specify.prep_met thy "met_eq_lin" [] Celem.e_metID
    1.22        (["LinEq","solve_lineq_equation"],