1.1 --- a/src/Tools/isac/Knowledge/LinEq.thy	Sat Jun 22 13:15:52 2019 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/LinEq.thy	Sat Jun 22 14:34:06 2019 +0200
     1.3 @@ -9,12 +9,6 @@
     1.4  
     1.5  theory LinEq imports Poly Equation begin
     1.6  
     1.7 -consts
     1.8 -   Solve'_lineq'_equation
     1.9 -             :: "[bool,real, 
    1.10 -		   bool list] => bool list"
    1.11 -               ("((Script Solve'_lineq'_equation (_ _ =))// (_))" 9)
    1.12 -
    1.13  axiomatization where
    1.14  (*-- normalise --*)
    1.15    (*WN0509 compare PolyEq.all_left "[|Not(b=!=0)|] ==> (a = b) = (a - b = 0)"*)
    1.16 @@ -162,18 +156,7 @@
    1.17            ("#Find",  ["solutions v_v'i'"])],
    1.18          {rew_ord' = "termlessI", rls' = LinEq_erls, srls = Rule.e_rls, prls = LinEq_prls, calc = [],
    1.19            crls = LinEq_crls, errpats = [], nrls = norm_Poly},
    1.20 -        @{thm solve_linear_equation.simps}
    1.21 -	    (*"Script Solve_lineq_equation (e_e::bool) (v_v::real) =                 " ^
    1.22 -          "(let e_e =((Try         (Rewrite     ''all_left''            False)) @@   " ^ 
    1.23 -          "           (Try (Repeat (Rewrite     ''makex1_x''            False))) @@  " ^ 
    1.24 -          "           (Try         (Rewrite_Set ''expand_binoms''       False)) @@   " ^ 
    1.25 -          "           (Try (Repeat (Rewrite_Set_Inst [(''bdv'', v_v::real)]          " ^
    1.26 -          "                                 ''make_ratpoly_in''    False)))    @@    " ^
    1.27 -          "           (Try (Repeat (Rewrite_Set ''LinPoly_simplify''     False))))e_e;" ^
    1.28 -          "     e_e = ((Try (Rewrite_Set_Inst [(''bdv'', v_v::real)]                  " ^
    1.29 -          "                                     ''LinEq_simplify'' True)) @@  " ^
    1.30 -          "            (Repeat(Try (Rewrite_Set ''LinPoly_simplify''     False)))) e_e " ^
    1.31 -          " in ((Or_to_List e_e)::bool list))"*))]
    1.32 +        @{thm solve_linear_equation.simps})]
    1.33  \<close>
    1.34  ML \<open>Specify.get_met' @{theory} ["LinEq","solve_lineq_equation"];\<close>
    1.35