1.1 --- a/src/Tools/isac/Knowledge/LinEq.thy Thu Dec 20 18:02:25 2018 +0100
1.2 +++ b/src/Tools/isac/Knowledge/LinEq.thy Wed Dec 26 14:24:05 2018 +0100
1.3 @@ -149,15 +149,15 @@
1.4 {rew_ord' = "termlessI", rls' = LinEq_erls, srls = Rule.e_rls, prls = LinEq_prls, calc = [],
1.5 crls = LinEq_crls, errpats = [], nrls = norm_Poly},
1.6 "Script Solve_lineq_equation (e_e::bool) (v_v::real) = " ^
1.7 - "(let e_e =((Try (Rewrite all_left False)) @@ " ^
1.8 - " (Try (Repeat (Rewrite makex1_x False))) @@ " ^
1.9 - " (Try (Rewrite_Set expand_binoms False)) @@ " ^
1.10 - " (Try (Repeat (Rewrite_Set_Inst [(bdv, v_v::real)] " ^
1.11 - " make_ratpoly_in False))) @@ " ^
1.12 - " (Try (Repeat (Rewrite_Set LinPoly_simplify False))))e_e;" ^
1.13 - " e_e = ((Try (Rewrite_Set_Inst [(bdv, v_v::real)] " ^
1.14 - " LinEq_simplify True)) @@ " ^
1.15 - " (Repeat(Try (Rewrite_Set LinPoly_simplify False)))) e_e " ^
1.16 + "(let e_e =((Try (Rewrite ''all_left'' False)) @@ " ^
1.17 + " (Try (Repeat (Rewrite ''makex1_x'' False))) @@ " ^
1.18 + " (Try (Rewrite_Set ''expand_binoms'' False)) @@ " ^
1.19 + " (Try (Repeat (Rewrite_Set_Inst [(''bdv'', v_v::real)] " ^
1.20 + " ''make_ratpoly_in'' False))) @@ " ^
1.21 + " (Try (Repeat (Rewrite_Set ''LinPoly_simplify'' False))))e_e;" ^
1.22 + " e_e = ((Try (Rewrite_Set_Inst [(''bdv'', v_v::real)] " ^
1.23 + " ''LinEq_simplify'' True)) @@ " ^
1.24 + " (Repeat(Try (Rewrite_Set ''LinPoly_simplify'' False)))) e_e " ^
1.25 " in ((Or_to_List e_e)::bool list))")]
1.26 \<close>
1.27 ML \<open>Specify.get_met' @{theory} ["LinEq","solve_lineq_equation"];\<close>