src/Tools/isac/Knowledge/LinEq.thy
changeset 60449 2406d378cede
parent 60405 d4ebe139100d
child 60509 2e0b7ca391dc
equal deleted inserted replaced
60448:ae5f26c14181 60449:2406d378cede
   103 (*----------------------------- problems --------------------------------*)
   103 (*----------------------------- problems --------------------------------*)
   104 (* ---------linear----------- *)
   104 (* ---------linear----------- *)
   105 
   105 
   106 problem pbl_equ_univ_lin : "LINEAR/univariate/equation" =
   106 problem pbl_equ_univ_lin : "LINEAR/univariate/equation" =
   107   \<open>LinEq_prls\<close>
   107   \<open>LinEq_prls\<close>
   108   Method: "LinEq/solve_lineq_equation"
   108   Method_Ref: "LinEq/solve_lineq_equation"
   109   CAS: "solve (e_e::bool, v_v)"
   109   CAS: "solve (e_e::bool, v_v)"
   110   Given: "equality e_e" "solveFor v_v"
   110   Given: "equality e_e" "solveFor v_v"
   111   Where: "HOL.False" (*WN0509 just detected: this pbl can never be used?!?*)
   111   Where: "HOL.False" (*WN0509 just detected: this pbl can never be used?!?*)
   112     "Not( (lhs e_e) is_polyrat_in v_v)"
   112     "Not( (lhs e_e) is_polyrat_in v_v)"
   113     "Not( (rhs e_e) is_polyrat_in v_v)"
   113     "Not( (rhs e_e) is_polyrat_in v_v)"