1.1 --- a/src/Tools/isac/Knowledge/LinEq.thy	Tue May 28 16:52:30 2019 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/LinEq.thy	Wed May 29 10:36:16 2019 +0200
     1.3 @@ -137,10 +137,10 @@
     1.4        (["LinEq"], [],
     1.5          {rew_ord' = "tless_true",rls' = Atools_erls,calc = [], srls = Rule.e_rls, prls = Rule.e_rls,
     1.6            crls = LinEq_crls, errpats = [], nrls = norm_Poly},
     1.7 -        "empty_script")]
     1.8 +        @{thm refl})]
     1.9  \<close>
    1.10      (* ansprechen mit ["LinEq","solve_univar_equation"] *)
    1.11 -(*ok
    1.12 +
    1.13  partial_function (tailrec) solve_linear_equation :: "bool \<Rightarrow> real \<Rightarrow> bool list"
    1.14    where
    1.15  "solve_linear_equation e_e v_v =
    1.16 @@ -154,7 +154,6 @@
    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 -*)
    1.21  setup \<open>KEStore_Elems.add_mets
    1.22      [Specify.prep_met thy "met_eq_lin" [] Celem.e_metID
    1.23        (["LinEq","solve_lineq_equation"],
    1.24 @@ -163,7 +162,8 @@
    1.25            ("#Find",  ["solutions v_v'i'"])],
    1.26          {rew_ord' = "termlessI", rls' = LinEq_erls, srls = Rule.e_rls, prls = LinEq_prls, calc = [],
    1.27            crls = LinEq_crls, errpats = [], nrls = norm_Poly},
    1.28 -        "Script Solve_lineq_equation (e_e::bool) (v_v::real) =                 " ^
    1.29 +        @{thm solve_linear_equation.simps}
    1.30 +	    (*"Script Solve_lineq_equation (e_e::bool) (v_v::real) =                 " ^
    1.31            "(let e_e =((Try         (Rewrite     ''all_left''            False)) @@   " ^ 
    1.32            "           (Try (Repeat (Rewrite     ''makex1_x''            False))) @@  " ^ 
    1.33            "           (Try         (Rewrite_Set ''expand_binoms''       False)) @@   " ^ 
    1.34 @@ -173,7 +173,7 @@
    1.35            "     e_e = ((Try (Rewrite_Set_Inst [(''bdv'', v_v::real)]                  " ^
    1.36            "                                     ''LinEq_simplify'' True)) @@  " ^
    1.37            "            (Repeat(Try (Rewrite_Set ''LinPoly_simplify''     False)))) e_e " ^
    1.38 -          " in ((Or_to_List e_e)::bool list))")]
    1.39 +          " in ((Or_to_List e_e)::bool list))"*))]
    1.40  \<close>
    1.41  ML \<open>Specify.get_met' @{theory} ["LinEq","solve_lineq_equation"];\<close>
    1.42