521 ("#Find" ,["solutions v_v'i'"]) |
521 ("#Find" ,["solutions v_v'i'"]) |
522 ], |
522 ], |
523 RootEq_prls, SOME "solve (e_e::bool, v_v)", |
523 RootEq_prls, SOME "solve (e_e::bool, v_v)", |
524 [["RootEq","norm_sq_root_equation"]])); |
524 [["RootEq","norm_sq_root_equation"]])); |
525 *} |
525 *} |
526 setup {* KEStore_Elems.store_pbts |
526 setup {* KEStore_Elems.add_pbts |
527 [(prep_pbt thy "pbl_equ_univ_root" [] e_pblID |
527 [(prep_pbt thy "pbl_equ_univ_root" [] e_pblID |
528 (["root'","univariate","equation"], |
528 (["root'","univariate","equation"], |
529 [("#Given" ,["equality e_e","solveFor v_v"]), |
529 [("#Given" ,["equality e_e","solveFor v_v"]), |
530 ("#Where" ,["(lhs e_e) is_rootTerm_in (v_v::real) | " ^ |
530 ("#Where" ,["(lhs e_e) is_rootTerm_in (v_v::real) | " ^ |
531 "(rhs e_e) is_rootTerm_in (v_v::real)"]), |
531 "(rhs e_e) is_rootTerm_in (v_v::real)"]), |