1.1 --- a/src/Tools/isac/Knowledge/LinEq.thy	Tue Feb 19 19:35:12 2019 +0100
     1.2 +++ b/src/Tools/isac/Knowledge/LinEq.thy	Thu Feb 28 12:14:32 2019 +0100
     1.3 @@ -140,6 +140,7 @@
     1.4          "empty_script")]
     1.5  \<close>
     1.6      (* ansprechen mit ["LinEq","solve_univar_equation"] *)
     1.7 +(*ok
     1.8  partial_function (tailrec) solve_linear_equation :: "bool \<Rightarrow> real \<Rightarrow> bool list"
     1.9    where
    1.10  "solve_linear_equation e_e v_v =
    1.11 @@ -153,6 +154,7 @@
    1.12                                       ''LinEq_simplify'' True)) @@
    1.13              (Repeat(Try (Rewrite_Set ''LinPoly_simplify''    False)))) e_e
    1.14   in Or_to_List e_e)"
    1.15 +*)
    1.16  setup \<open>KEStore_Elems.add_mets
    1.17      [Specify.prep_met thy "met_eq_lin" [] Celem.e_metID
    1.18        (["LinEq","solve_lineq_equation"],