src/Tools/isac/Knowledge/Equation.thy
changeset 59903 5037ca1b112b
parent 59898 68883c046963
child 59962 6a59d252345d
     1.1 --- a/src/Tools/isac/Knowledge/Equation.thy	Wed Apr 22 11:23:30 2020 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Equation.thy	Wed Apr 22 14:36:27 2020 +0200
     1.3 @@ -43,14 +43,14 @@
     1.4  setup \<open>KEStore_Elems.add_rlss [("univariate_equation_prls",
     1.5    (Context.theory_name @{theory}, Auto_Prog.prep_rls @{theory} univariate_equation_prls))]\<close>
     1.6  setup \<open>KEStore_Elems.add_pbts
     1.7 -  [(Specify.prep_pbt thy "pbl_equ" [] Spec.e_pblID
     1.8 +  [(Specify.prep_pbt thy "pbl_equ" [] Problem.id_empty
     1.9        (["equation"],
    1.10          [("#Given" ,["equality e_e","solveFor v_v"]),
    1.11            ("#Where" ,["matches (?a = ?b) e_e"]),
    1.12            ("#Find"  ,["solutions v_v'i'"])],
    1.13          Rule_Set.append_rules "equation_prls" Rule_Set.empty  [Rule.Eval ("Prog_Expr.matches", Prog_Expr.eval_matches "")],
    1.14          SOME "solve (e_e::bool, v_v)", [])),
    1.15 -    (Specify.prep_pbt thy "pbl_equ_univ" [] Spec.e_pblID
    1.16 +    (Specify.prep_pbt thy "pbl_equ_univ" [] Problem.id_empty
    1.17        (["univariate","equation"],
    1.18          [("#Given" ,["equality e_e","solveFor v_v"]),
    1.19            ("#Where" ,["matches (?a = ?b) e_e"]),
    1.20 @@ -81,7 +81,7 @@
    1.21  
    1.22  
    1.23  setup \<open>KEStore_Elems.add_mets
    1.24 -    [Specify.prep_met thy "met_equ" [] Spec.e_metID
    1.25 +    [Specify.prep_met thy "met_equ" [] Method.id_empty
    1.26  	    (["Equation"], [],
    1.27  	      {rew_ord'="tless_true", rls'=Rule_Set.Empty, calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty, crls = Atools_erls,
    1.28            errpats = [], nrls = Rule_Set.empty},