equal
deleted
inserted
replaced
44 val univariate_equation_prls = |
44 val univariate_equation_prls = |
45 append_rls "univariate_equation_prls" e_rls |
45 append_rls "univariate_equation_prls" e_rls |
46 [Calc ("Tools.matches",eval_matches "")]; |
46 [Calc ("Tools.matches",eval_matches "")]; |
47 *} |
47 *} |
48 setup {* KEStore_Elems.add_rlss [("univariate_equation_prls", |
48 setup {* KEStore_Elems.add_rlss [("univariate_equation_prls", |
49 (Context.theory_name @{theory}, prep_rls univariate_equation_prls))] *} |
49 (Context.theory_name @{theory}, prep_rls @{theory} univariate_equation_prls))] *} |
50 setup {* KEStore_Elems.add_pbts |
50 setup {* KEStore_Elems.add_pbts |
51 [(prep_pbt thy "pbl_equ" [] e_pblID |
51 [(prep_pbt thy "pbl_equ" [] e_pblID |
52 (["equation"], |
52 (["equation"], |
53 [("#Given" ,["equality e_e","solveFor v_v"]), |
53 [("#Given" ,["equality e_e","solveFor v_v"]), |
54 ("#Where" ,["matches (?a = ?b) e_e"]), |
54 ("#Where" ,["matches (?a = ?b) e_e"]), |