src/Tools/isac/Knowledge/LinEq.thy
changeset 60449 2406d378cede
parent 60405 d4ebe139100d
child 60509 2e0b7ca391dc
     1.1 --- a/src/Tools/isac/Knowledge/LinEq.thy	Wed Jun 01 13:39:41 2022 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/LinEq.thy	Wed Jun 01 14:17:23 2022 +0200
     1.3 @@ -105,7 +105,7 @@
     1.4  
     1.5  problem pbl_equ_univ_lin : "LINEAR/univariate/equation" =
     1.6    \<open>LinEq_prls\<close>
     1.7 -  Method: "LinEq/solve_lineq_equation"
     1.8 +  Method_Ref: "LinEq/solve_lineq_equation"
     1.9    CAS: "solve (e_e::bool, v_v)"
    1.10    Given: "equality e_e" "solveFor v_v"
    1.11    Where: "HOL.False" (*WN0509 just detected: this pbl can never be used?!?*)