1.1 --- a/src/Tools/isac/Knowledge/LinEq.thy	Sun Jun 20 12:45:03 2021 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/LinEq.thy	Sun Jun 20 16:26:18 2021 +0200
     1.3 @@ -106,19 +106,20 @@
     1.4  \<close>
     1.5  rule_set_knowledge LinEq_simplify = LinEq_simplify
     1.6  
     1.7 -(*----------------------------- problem types --------------------------------*)
     1.8 +(*----------------------------- problems --------------------------------*)
     1.9  (* ---------linear----------- *)
    1.10 -setup \<open>KEStore_Elems.add_pbts
    1.11 -  [(Problem.prep_input @{theory} "pbl_equ_univ_lin" [] Problem.id_empty
    1.12 -      (["LINEAR", "univariate", "equation"],
    1.13 -        [("#Given" ,["equality e_e", "solveFor v_v"]),
    1.14 -          ("#Where" ,["HOL.False", (*WN0509 just detected: this pbl can never be used?!?*)
    1.15 -              "Not( (lhs e_e) is_polyrat_in v_v)",
    1.16 -              "Not( (rhs e_e) is_polyrat_in v_v)",
    1.17 -              "((lhs e_e) has_degree_in v_v)=1",
    1.18 -	            "((rhs e_e) has_degree_in v_v)=1"]),
    1.19 -          ("#Find"  ,["solutions v_v'i'"])],
    1.20 -        LinEq_prls, SOME "solve (e_e::bool, v_v)", [["LinEq", "solve_lineq_equation"]]))]\<close>
    1.21 +
    1.22 +problem pbl_equ_univ_lin : "LINEAR/univariate/equation" =
    1.23 +  \<open>LinEq_prls\<close>
    1.24 +  Method: "LinEq/solve_lineq_equation"
    1.25 +  CAS: "solve (e_e::bool, v_v)"
    1.26 +  Given: "equality e_e" "solveFor v_v"
    1.27 +  Where: "HOL.False" (*WN0509 just detected: this pbl can never be used?!?*)
    1.28 +    "Not( (lhs e_e) is_polyrat_in v_v)"
    1.29 +    "Not( (rhs e_e) is_polyrat_in v_v)"
    1.30 +    "((lhs e_e) has_degree_in v_v)=1"
    1.31 +	  "((rhs e_e) has_degree_in v_v)=1"
    1.32 +  Find: "solutions v_v'i'"
    1.33  
    1.34  (*-------------- methods------------------------------------------------------*)
    1.35  method met_eqlin : "LinEq" =