1.1 --- a/src/Tools/isac/Knowledge/AlgEin.thy Thu Jun 10 11:54:20 2021 +0200
1.2 +++ b/src/Tools/isac/Knowledge/AlgEin.thy Thu Jun 10 12:23:57 2021 +0200
1.3 @@ -24,8 +24,8 @@
1.4 \<close>
1.5 (** problems **)
1.6 setup \<open>KEStore_Elems.add_pbts
1.7 - [(Problem.prep_input thy "pbl_algein" [] Problem.id_empty (["Berechnung"], [], Rule_Set.empty, NONE, [])),
1.8 - (Problem.prep_input thy "pbl_algein_numsym" [] Problem.id_empty
1.9 + [(Problem.prep_input @{theory} "pbl_algein" [] Problem.id_empty (["Berechnung"], [], Rule_Set.empty, NONE, [])),
1.10 + (Problem.prep_input @{theory} "pbl_algein_numsym" [] Problem.id_empty
1.11 (["numerischSymbolische", "Berechnung"],
1.12 [("#Given",
1.13 ["KantenLaenge k_k", "Querschnitt q__q"(*q_ in Biegelinie.thy*), "KantenUnten u_u",
1.14 @@ -34,12 +34,12 @@
1.15 Rule_Set.empty, NONE, [["Berechnung", "erstNumerisch"], ["Berechnung", "erstSymbolisch"]]))]\<close>
1.16
1.17 setup \<open>KEStore_Elems.add_mets
1.18 - [MethodC.prep_input thy "met_algein" [] MethodC.id_empty
1.19 + [MethodC.prep_input @{theory} "met_algein" [] MethodC.id_empty
1.20 (["Berechnung"], [],
1.21 {rew_ord'="tless_true", rls'= Rule_Set.Empty, calc = [], srls = Rule_Set.Empty, prls = Rule_Set.Empty, crls =Rule_Set.Empty,
1.22 errpats = [], nrls = Rule_Set.Empty},
1.23 @{thm refl}),
1.24 - MethodC.prep_input thy "met_algein_numsym" [] MethodC.id_empty
1.25 + MethodC.prep_input @{theory} "met_algein_numsym" [] MethodC.id_empty
1.26 (["Berechnung", "erstNumerisch"], [],
1.27 {rew_ord'="tless_true", rls'= Rule_Set.Empty, calc = [], srls = Rule_Set.Empty, prls = Rule_Set.Empty, crls =Rule_Set.Empty,
1.28 errpats = [], nrls = Rule_Set.Empty},
1.29 @@ -69,7 +69,7 @@
1.30 in
1.31 Try (Rewrite_Set ''norm_Poly'') t_t)"
1.32 setup \<open>KEStore_Elems.add_mets
1.33 - [MethodC.prep_input thy "met_algein_numsym_1num" [] MethodC.id_empty
1.34 + [MethodC.prep_input @{theory} "met_algein_numsym_1num" [] MethodC.id_empty
1.35 (["Berechnung", "erstNumerisch"],
1.36 [("#Given" ,["KantenLaenge k_k", "Querschnitt q__q", "KantenUnten u_u",
1.37 "KantenSenkrecht s_s", "KantenOben o_o"]),
1.38 @@ -102,7 +102,7 @@
1.39 in
1.40 (Try (Rewrite_Set ''norm_Poly'')) t_t)"
1.41 setup \<open>KEStore_Elems.add_mets
1.42 - [MethodC.prep_input thy "met_algein_symnum" [] MethodC.id_empty
1.43 + [MethodC.prep_input @{theory} "met_algein_symnum" [] MethodC.id_empty
1.44 (["Berechnung", "erstSymbolisch"],
1.45 [("#Given" ,["KantenLaenge k_k", "Querschnitt q__q", "KantenUnten u_u",
1.46 "KantenSenkrecht s_s", "KantenOben o_o"]),
2.1 --- a/src/Tools/isac/Knowledge/Diff.thy Thu Jun 10 11:54:20 2021 +0200
2.2 +++ b/src/Tools/isac/Knowledge/Diff.thy Thu Jun 10 12:23:57 2021 +0200
2.3 @@ -241,8 +241,8 @@
2.4
2.5 (** problem types **)
2.6 setup \<open>KEStore_Elems.add_pbts
2.7 - [(Problem.prep_input thy "pbl_fun" [] Problem.id_empty (["function"], [], Rule_Set.empty, NONE, [])),
2.8 - (Problem.prep_input thy "pbl_fun_deriv" [] Problem.id_empty
2.9 + [(Problem.prep_input @{theory} "pbl_fun" [] Problem.id_empty (["function"], [], Rule_Set.empty, NONE, [])),
2.10 + (Problem.prep_input @{theory} "pbl_fun_deriv" [] Problem.id_empty
2.11 (["derivative_of", "function"],
2.12 [("#Given" ,["functionTerm f_f", "differentiateFor v_v"]),
2.13 ("#Find" ,["derivative f_f'"])],
2.14 @@ -250,7 +250,7 @@
2.15 SOME "Diff (f_f, v_v)", [["diff", "differentiate_on_R"],
2.16 ["diff", "after_simplification"]])),
2.17 (*here "named" is used differently from Integration"*)
2.18 - (Problem.prep_input thy "pbl_fun_deriv_nam" [] Problem.id_empty
2.19 + (Problem.prep_input @{theory} "pbl_fun_deriv_nam" [] Problem.id_empty
2.20 (["named", "derivative_of", "function"],
2.21 [("#Given" ,["functionEq f_f", "differentiateFor v_v"]),
2.22 ("#Find" ,["derivativeEq f_f'"])],
2.23 @@ -274,7 +274,7 @@
2.24 | argl2dtss _ = raise ERROR "Diff.ML: wrong argument for argl2dtss";
2.25 \<close>
2.26 setup \<open>KEStore_Elems.add_mets
2.27 - [MethodC.prep_input thy "met_diff" [] MethodC.id_empty
2.28 + [MethodC.prep_input @{theory} "met_diff" [] MethodC.id_empty
2.29 (["diff"], [],
2.30 {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty,
2.31 crls = Atools_erls, errpats = [], nrls = norm_diff},
2.32 @@ -309,7 +309,7 @@
2.33 Try (Rewrite_Set_Inst [(''bdv'',v_v)] ''diff_sym_conv''))
2.34 ) f_f')"
2.35 setup \<open>KEStore_Elems.add_mets
2.36 - [MethodC.prep_input thy "met_diff_onR" [] MethodC.id_empty
2.37 + [MethodC.prep_input @{theory} "met_diff_onR" [] MethodC.id_empty
2.38 (["diff", "differentiate_on_R"],
2.39 [("#Given" ,["functionTerm f_f", "differentiateFor v_v"]),
2.40 ("#Find" ,["derivative f_f'"])],
2.41 @@ -344,7 +344,7 @@
2.42 (Repeat (Rewrite_Set ''make_polynomial'')))
2.43 ) f_f')"
2.44 setup \<open>KEStore_Elems.add_mets
2.45 - [MethodC.prep_input thy "met_diff_simpl" [] MethodC.id_empty
2.46 + [MethodC.prep_input @{theory} "met_diff_simpl" [] MethodC.id_empty
2.47 (["diff", "diff_simpl"],
2.48 [("#Given", ["functionTerm f_f", "differentiateFor v_v"]),
2.49 ("#Find" , ["derivative f_f'"])],
2.50 @@ -382,7 +382,7 @@
2.51 Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''diff_sym_conv'' ))
2.52 ) f_f')"
2.53 setup \<open>KEStore_Elems.add_mets
2.54 - [MethodC.prep_input thy "met_diff_equ" [] MethodC.id_empty
2.55 + [MethodC.prep_input @{theory} "met_diff_equ" [] MethodC.id_empty
2.56 (["diff", "differentiate_equality"],
2.57 [("#Given" ,["functionEq f_f", "differentiateFor v_v"]),
2.58 ("#Find" ,["derivativeEq f_f'"])],
2.59 @@ -405,7 +405,7 @@
2.60 ) term')"
2.61
2.62 setup \<open>KEStore_Elems.add_mets
2.63 - [MethodC.prep_input thy "met_diff_after_simp" [] MethodC.id_empty
2.64 + [MethodC.prep_input @{theory} "met_diff_after_simp" [] MethodC.id_empty
2.65 (["diff", "after_simplification"],
2.66 [("#Given" ,["functionTerm term", "differentiateFor bound_variable"]),
2.67 ("#Find" ,["derivative term'"])],
2.68 @@ -414,7 +414,7 @@
2.69 @{thm simplify_derivative.simps})]
2.70 \<close>
2.71 setup \<open>KEStore_Elems.add_cas
2.72 - [((Thm.term_of o the o (TermC.parse thy)) "Diff",
2.73 + [((Thm.term_of o the o (TermC.parse @{theory})) "Diff",
2.74 (("Isac_Knowledge", ["derivative_of", "function"], ["no_met"]), argl2dtss))]\<close>
2.75 ML \<open>
2.76
2.77 @@ -431,7 +431,7 @@
2.78 | argl2dtss _ = raise ERROR "Diff.ML: wrong argument for argl2dtss";
2.79 \<close>
2.80 setup \<open>KEStore_Elems.add_cas
2.81 - [((Thm.term_of o the o (TermC.parse thy)) "Differentiate",
2.82 + [((Thm.term_of o the o (TermC.parse @{theory})) "Differentiate",
2.83 (("Isac_Knowledge", ["named", "derivative_of", "function"], ["no_met"]), argl2dtss))]
2.84 \<close> ML \<open>
2.85 \<close> ML \<open>
3.1 --- a/src/Tools/isac/Knowledge/DiffApp.thy Thu Jun 10 11:54:20 2021 +0200
3.2 +++ b/src/Tools/isac/Knowledge/DiffApp.thy Thu Jun 10 12:23:57 2021 +0200
3.3 @@ -63,37 +63,37 @@
3.4
3.5 (** problem types **)
3.6 setup \<open>KEStore_Elems.add_pbts
3.7 - [(Problem.prep_input thy "pbl_fun_max" [] Problem.id_empty
3.8 + [(Problem.prep_input @{theory} "pbl_fun_max" [] Problem.id_empty
3.9 (["maximum_of", "function"],
3.10 [("#Given" ,["fixedValues f_ix"]),
3.11 ("#Find" ,["maximum m_m", "valuesFor v_s"]),
3.12 ("#Relate",["relations r_s"])],
3.13 Rule_Set.empty, NONE, [])),
3.14 - (Problem.prep_input thy "pbl_fun_make" [] Problem.id_empty
3.15 + (Problem.prep_input @{theory} "pbl_fun_make" [] Problem.id_empty
3.16 (["make", "function"],
3.17 [("#Given" ,["functionOf f_f", "boundVariable v_v", "equalities eqs"]),
3.18 ("#Find" ,["functionEq f_1"])],
3.19 Rule_Set.empty, NONE, [])),
3.20 - (Problem.prep_input thy "pbl_fun_max_expl" [] Problem.id_empty
3.21 + (Problem.prep_input @{theory} "pbl_fun_max_expl" [] Problem.id_empty
3.22 (["by_explicit", "make", "function"],
3.23 [("#Given" ,["functionOf f_f", "boundVariable v_v", "equalities eqs"]),
3.24 ("#Find" ,["functionEq f_1"])],
3.25 Rule_Set.empty, NONE, [["DiffApp", "make_fun_by_explicit"]])),
3.26 - (Problem.prep_input thy "pbl_fun_max_newvar" [] Problem.id_empty
3.27 + (Problem.prep_input @{theory} "pbl_fun_max_newvar" [] Problem.id_empty
3.28 (["by_new_variable", "make", "function"],
3.29 [("#Given" ,["functionOf f_f", "boundVariable v_v", "equalities eqs"]),
3.30 (*WN.12.5.03: precond for distinction still missing*)
3.31 ("#Find" ,["functionEq f_1"])],
3.32 Rule_Set.empty, NONE, [["DiffApp", "make_fun_by_new_variable"]])),
3.33 - (Problem.prep_input thy "pbl_fun_max_interv" [] Problem.id_empty
3.34 + (Problem.prep_input @{theory} "pbl_fun_max_interv" [] Problem.id_empty
3.35 (["on_interval", "maximum_of", "function"],
3.36 [("#Given" ,["functionEq t_t", "boundVariable v_v", "interval i_tv"]),
3.37 (*WN.12.5.03: precond for distinction still missing*)
3.38 ("#Find" ,["maxArgument v_0"])],
3.39 Rule_Set.empty, NONE, [])),
3.40 - (Problem.prep_input thy "pbl_tool" [] Problem.id_empty
3.41 + (Problem.prep_input @{theory} "pbl_tool" [] Problem.id_empty
3.42 (["tool"], [], Rule_Set.empty, NONE, [])),
3.43 - (Problem.prep_input thy "pbl_tool_findvals" [] Problem.id_empty
3.44 + (Problem.prep_input @{theory} "pbl_tool_findvals" [] Problem.id_empty
3.45 (["find_values", "tool"],
3.46 [("#Given" ,["maxArgument m_ax", "functionEq f_f", "boundVariable v_v"]),
3.47 ("#Find" ,["valuesFor v_ls"]),
3.48 @@ -103,7 +103,7 @@
3.49
3.50 (** methods, scripts not yet implemented **)
3.51 setup \<open>KEStore_Elems.add_mets
3.52 - [MethodC.prep_input thy "met_diffapp" [] MethodC.id_empty
3.53 + [MethodC.prep_input @{theory} "met_diffapp" [] MethodC.id_empty
3.54 (["DiffApp"], [],
3.55 {rew_ord'="tless_true", rls'=Atools_erls,calc = [], srls = Rule_Set.empty, prls = Rule_Set.empty,
3.56 crls = Atools_erls, errpats = [], nrls = norm_Rational (*, asm_rls=[],asm_thm=[]*)},
3.57 @@ -125,7 +125,7 @@
3.58 in SubProblem (''DiffApp'',[''find_values'', ''tool''], [''Isac_Knowledge'', ''find_values''])
3.59 [REAL m_x, REAL (rhs t_t), REAL v_v, REAL m_m, BOOL_LIST (dropWhile (ident e_e) r_s)])"
3.60 setup \<open>KEStore_Elems.add_mets
3.61 - [MethodC.prep_input thy "met_diffapp_max" [] MethodC.id_empty
3.62 + [MethodC.prep_input @{theory} "met_diffapp_max" [] MethodC.id_empty
3.63 (["DiffApp", "max_by_calculus"],
3.64 [("#Given" ,["fixedValues f_ix", "maximum m_m", "relations r_s", "boundVariable v_v",
3.65 "interval i_tv", "errorBound e_rr"]),
3.66 @@ -152,7 +152,7 @@
3.67 [BOOL e_2, REAL v_2]
3.68 in Substitute [(v_1 = (rhs o hd) s_1), (v_2 = (rhs o hd) s_2)] h_h)"
3.69 setup \<open>KEStore_Elems.add_mets
3.70 - [MethodC.prep_input thy "met_diffapp_funnew" [] MethodC.id_empty
3.71 + [MethodC.prep_input @{theory} "met_diffapp_funnew" [] MethodC.id_empty
3.72 (["DiffApp", "make_fun_by_new_variable"],
3.73 [("#Given" ,["functionOf f_f", "boundVariable v_v", "equalities eqs"]),
3.74 ("#Find" ,["functionEq f_1"])],
3.75 @@ -172,7 +172,7 @@
3.76 [BOOL e_1, REAL v_1]
3.77 in Substitute [(v_1 = (rhs o hd) s_1)] h_h) "
3.78 setup \<open>KEStore_Elems.add_mets
3.79 - [MethodC.prep_input thy "met_diffapp_funexp" [] MethodC.id_empty
3.80 + [MethodC.prep_input @{theory} "met_diffapp_funexp" [] MethodC.id_empty
3.81 (["DiffApp", "make_fun_by_explicit"],
3.82 [("#Given" ,["functionOf f_f", "boundVariable v_v", "equalities eqs"]),
3.83 ("#Find" ,["functionEq f_1"])],
3.84 @@ -181,14 +181,14 @@
3.85 @{thm make_fun_by_explicit.simps})]
3.86 \<close>
3.87 setup \<open>KEStore_Elems.add_mets
3.88 - [MethodC.prep_input thy "met_diffapp_max_oninterval" [] MethodC.id_empty
3.89 + [MethodC.prep_input @{theory} "met_diffapp_max_oninterval" [] MethodC.id_empty
3.90 (["DiffApp", "max_on_interval_by_calculus"],
3.91 [("#Given" ,["functionEq t_t", "boundVariable v_v", "interval i_tv"(*, "errorBound e_rr"*)]),
3.92 ("#Find" ,["maxArgument v_0"])],
3.93 {rew_ord'="tless_true",rls'=eval_rls,calc=[],srls = Rule_Set.empty,prls=Rule_Set.empty, crls = eval_rls,
3.94 errpats = [], nrls = norm_Rational (*, asm_rls=[],asm_thm=[]*)},
3.95 @{thm refl}),
3.96 - MethodC.prep_input thy "met_diffapp_findvals" [] MethodC.id_empty
3.97 + MethodC.prep_input @{theory} "met_diffapp_findvals" [] MethodC.id_empty
3.98 (["DiffApp", "find_values"], [],
3.99 {rew_ord'="tless_true",rls'=eval_rls,calc=[],srls = Rule_Set.empty,prls=Rule_Set.empty, crls = eval_rls,
3.100 errpats = [], nrls = norm_Rational(*, asm_rls = [], asm_thm = []*)},
4.1 --- a/src/Tools/isac/Knowledge/DiophantEq.thy Thu Jun 10 11:54:20 2021 +0200
4.2 +++ b/src/Tools/isac/Knowledge/DiophantEq.thy Thu Jun 10 12:23:57 2021 +0200
4.3 @@ -15,7 +15,7 @@
4.4
4.5 text \<open>problemclass for the usecase\<close>
4.6 setup \<open>KEStore_Elems.add_pbts
4.7 - [(Problem.prep_input thy "pbl_equ_dio" [] Problem.id_empty
4.8 + [(Problem.prep_input @{theory} "pbl_equ_dio" [] Problem.id_empty
4.9 (["diophantine", "equation"],
4.10 [("#Given" ,["boolTestGiven e_e", "intTestGiven (v_v::int)"]),
4.11 (* TODO: drop ^^^^^*)
4.12 @@ -33,7 +33,7 @@
4.13 (Try (Calculate ''PLUS'')) #>
4.14 (Try (Calculate ''TIMES''))) e_e)"
4.15 setup \<open>KEStore_Elems.add_mets
4.16 - [MethodC.prep_input thy "met_test_diophant" [] MethodC.id_empty
4.17 + [MethodC.prep_input @{theory} "met_test_diophant" [] MethodC.id_empty
4.18 (["Test", "solve_diophant"],
4.19 [("#Given" ,["boolTestGiven e_e", "intTestGiven (v_v::int)"]),
4.20 (* TODO: drop ^^^^^*)
5.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy Thu Jun 10 11:54:20 2021 +0200
5.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy Thu Jun 10 12:23:57 2021 +0200
5.3 @@ -407,18 +407,18 @@
5.4 section \<open>Problems\<close>
5.5
5.6 setup \<open>KEStore_Elems.add_pbts
5.7 - [(Problem.prep_input thy "pbl_equsys" [] Problem.id_empty
5.8 + [(Problem.prep_input @{theory} "pbl_equsys" [] Problem.id_empty
5.9 (["system"],
5.10 [("#Given" ,["equalities e_s", "solveForVars v_s"]),
5.11 ("#Find" ,["solution ss'''"](*''' is copy-named*))],
5.12 Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)], SOME "solveSystem e_s v_s", [])),
5.13 - (Problem.prep_input thy "pbl_equsys_lin" [] Problem.id_empty
5.14 + (Problem.prep_input @{theory} "pbl_equsys_lin" [] Problem.id_empty
5.15 (["LINEAR", "system"],
5.16 [("#Given" ,["equalities e_s", "solveForVars v_s"]),
5.17 (*TODO.WN050929 check linearity*)
5.18 ("#Find" ,["solution ss'''"])],
5.19 Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)], SOME "solveSystem e_s v_s", [])),
5.20 - (Problem.prep_input thy "pbl_equsys_lin_2x2" [] Problem.id_empty
5.21 + (Problem.prep_input @{theory} "pbl_equsys_lin_2x2" [] Problem.id_empty
5.22 (["2x2", "LINEAR", "system"],
5.23 (*~~~~~~~~~~~~~~~~~~~~~~~~~*)
5.24 [("#Given" ,["equalities e_s", "solveForVars v_s"]),
5.25 @@ -430,7 +430,7 @@
5.26 Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_"),
5.27 Rule.Eval ("HOL.eq", Prog_Expr.eval_equal "#equal_")],
5.28 SOME "solveSystem e_s v_s", [])),
5.29 - (Problem.prep_input thy "pbl_equsys_lin_2x2_tri" [] Problem.id_empty
5.30 + (Problem.prep_input @{theory} "pbl_equsys_lin_2x2_tri" [] Problem.id_empty
5.31 (["triangular", "2x2", "LINEAR", "system"],
5.32 [("#Given" ,["equalities e_s", "solveForVars v_s"]),
5.33 ("#Where",
5.34 @@ -438,14 +438,14 @@
5.35 " v_s from v_s occur_exactly_in (NTH 2 (e_s::bool list))"]),
5.36 ("#Find" ,["solution ss'''"])],
5.37 prls_triangular, SOME "solveSystem e_s v_s", [["EqSystem", "top_down_substitution", "2x2"]])),
5.38 - (Problem.prep_input thy "pbl_equsys_lin_2x2_norm" [] Problem.id_empty
5.39 + (Problem.prep_input @{theory} "pbl_equsys_lin_2x2_norm" [] Problem.id_empty
5.40 (["normalise", "2x2", "LINEAR", "system"],
5.41 [("#Given" ,["equalities e_s", "solveForVars v_s"]),
5.42 ("#Find" ,["solution ss'''"])],
5.43 Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)],
5.44 SOME "solveSystem e_s v_s",
5.45 [["EqSystem", "normalise", "2x2"]])),
5.46 - (Problem.prep_input thy "pbl_equsys_lin_3x3" [] Problem.id_empty
5.47 + (Problem.prep_input @{theory} "pbl_equsys_lin_3x3" [] Problem.id_empty
5.48 (["3x3", "LINEAR", "system"],
5.49 (*~~~~~~~~~~~~~~~~~~~~~~~~~*)
5.50 [("#Given" ,["equalities e_s", "solveForVars v_s"]),
5.51 @@ -457,7 +457,7 @@
5.52 Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_"),
5.53 Rule.Eval ("HOL.eq", Prog_Expr.eval_equal "#equal_")],
5.54 SOME "solveSystem e_s v_s", [])),
5.55 - (Problem.prep_input thy "pbl_equsys_lin_4x4" [] Problem.id_empty
5.56 + (Problem.prep_input @{theory} "pbl_equsys_lin_4x4" [] Problem.id_empty
5.57 (["4x4", "LINEAR", "system"],
5.58 (*~~~~~~~~~~~~~~~~~~~~~~~~~*)
5.59 [("#Given" ,["equalities e_s", "solveForVars v_s"]),
5.60 @@ -469,7 +469,7 @@
5.61 Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_"),
5.62 Rule.Eval ("HOL.eq", Prog_Expr.eval_equal "#equal_")],
5.63 SOME "solveSystem e_s v_s", [])),
5.64 - (Problem.prep_input thy "pbl_equsys_lin_4x4_tri" [] Problem.id_empty
5.65 + (Problem.prep_input @{theory} "pbl_equsys_lin_4x4_tri" [] Problem.id_empty
5.66 (["triangular", "4x4", "LINEAR", "system"],
5.67 [("#Given" ,["equalities e_s", "solveForVars v_s"]),
5.68 ("#Where" , (*accepts missing variables up to diagional form*)
5.69 @@ -482,7 +482,7 @@
5.70 [Rule.Eval ("Prog_Expr.occurs_in", Prog_Expr.eval_occurs_in "")],
5.71 SOME "solveSystem e_s v_s",
5.72 [["EqSystem", "top_down_substitution", "4x4"]])),
5.73 - (Problem.prep_input thy "pbl_equsys_lin_4x4_norm" [] Problem.id_empty
5.74 + (Problem.prep_input @{theory} "pbl_equsys_lin_4x4_norm" [] Problem.id_empty
5.75 (["normalise", "4x4", "LINEAR", "system"],
5.76 [("#Given" ,["equalities e_s", "solveForVars v_s"]),
5.77 (*Length is checked 1 level above*)
5.78 @@ -512,12 +512,12 @@
5.79 section \<open>Methods\<close>
5.80
5.81 setup \<open>KEStore_Elems.add_mets
5.82 - [MethodC.prep_input thy "met_eqsys" [] MethodC.id_empty
5.83 + [MethodC.prep_input @{theory} "met_eqsys" [] MethodC.id_empty
5.84 (["EqSystem"], [],
5.85 {rew_ord'="tless_true", rls' = Rule_Set.Empty, calc = [], srls = Rule_Set.Empty, prls = Rule_Set.Empty, crls = Rule_Set.Empty,
5.86 errpats = [], nrls = Rule_Set.Empty},
5.87 @{thm refl}),
5.88 - MethodC.prep_input thy "met_eqsys_topdown" [] MethodC.id_empty
5.89 + MethodC.prep_input @{theory} "met_eqsys_topdown" [] MethodC.id_empty
5.90 (["EqSystem", "top_down_substitution"], [],
5.91 {rew_ord'="tless_true", rls' = Rule_Set.Empty, calc = [], srls = Rule_Set.Empty, prls = Rule_Set.Empty, crls = Rule_Set.Empty,
5.92 errpats = [], nrls = Rule_Set.Empty},
5.93 @@ -544,7 +544,7 @@
5.94 in
5.95 Try (Rewrite_Set ''order_system'' ) e__s) "
5.96 setup \<open>KEStore_Elems.add_mets
5.97 - [MethodC.prep_input thy "met_eqsys_topdown_2x2" [] MethodC.id_empty
5.98 + [MethodC.prep_input @{theory} "met_eqsys_topdown_2x2" [] MethodC.id_empty
5.99 (["EqSystem", "top_down_substitution", "2x2"],
5.100 [("#Given", ["equalities e_s", "solveForVars v_s"]),
5.101 ("#Where",
5.102 @@ -560,7 +560,7 @@
5.103 @{thm solve_system.simps})]
5.104 \<close>
5.105 setup \<open>KEStore_Elems.add_mets
5.106 - [MethodC.prep_input thy "met_eqsys_norm" [] MethodC.id_empty
5.107 + [MethodC.prep_input @{theory} "met_eqsys_norm" [] MethodC.id_empty
5.108 (["EqSystem", "normalise"], [],
5.109 {rew_ord'="tless_true", rls' = Rule_Set.Empty, calc = [], srls = Rule_Set.Empty, prls = Rule_Set.Empty, crls = Rule_Set.Empty,
5.110 errpats = [], nrls = Rule_Set.Empty},
5.111 @@ -582,7 +582,7 @@
5.112 SubProblem (''EqSystem'', [''LINEAR'', ''system''], [''no_met''])
5.113 [BOOL_LIST e__s, REAL_LIST v_s])"
5.114 setup \<open>KEStore_Elems.add_mets
5.115 - [MethodC.prep_input thy "met_eqsys_norm_2x2" [] MethodC.id_empty
5.116 + [MethodC.prep_input @{theory} "met_eqsys_norm_2x2" [] MethodC.id_empty
5.117 (["EqSystem", "normalise", "2x2"],
5.118 [("#Given" ,["equalities e_s", "solveForVars v_s"]),
5.119 ("#Find" ,["solution ss'''"])],
5.120 @@ -614,7 +614,7 @@
5.121 SubProblem (''EqSystem'', [''LINEAR'', ''system''], [''no_met''])
5.122 [BOOL_LIST e__s, REAL_LIST v_s])"
5.123 setup \<open>KEStore_Elems.add_mets
5.124 - [MethodC.prep_input thy "met_eqsys_norm_4x4" [] MethodC.id_empty
5.125 + [MethodC.prep_input @{theory} "met_eqsys_norm_4x4" [] MethodC.id_empty
5.126 (["EqSystem", "normalise", "4x4"],
5.127 [("#Given" ,["equalities e_s", "solveForVars v_s"]),
5.128 ("#Find" ,["solution ss'''"])],
5.129 @@ -646,7 +646,7 @@
5.130 in
5.131 [e_1, e_2, NTH 3 e_s, NTH 4 e_s])"
5.132 setup \<open>KEStore_Elems.add_mets
5.133 - [MethodC.prep_input thy "met_eqsys_topdown_4x4" [] MethodC.id_empty
5.134 + [MethodC.prep_input @{theory} "met_eqsys_topdown_4x4" [] MethodC.id_empty
5.135 (["EqSystem", "top_down_substitution", "4x4"],
5.136 [("#Given" ,["equalities e_s", "solveForVars v_s"]),
5.137 ("#Where" , (*accepts missing variables up to diagonal form*)
6.1 --- a/src/Tools/isac/Knowledge/Equation.thy Thu Jun 10 11:54:20 2021 +0200
6.2 +++ b/src/Tools/isac/Knowledge/Equation.thy Thu Jun 10 12:23:57 2021 +0200
6.3 @@ -42,14 +42,14 @@
6.4 \<close>
6.5 rule_set_knowledge univariate_equation_prls = \<open>Auto_Prog.prep_rls @{theory} univariate_equation_prls\<close>
6.6 setup \<open>KEStore_Elems.add_pbts
6.7 - [(Problem.prep_input thy "pbl_equ" [] Problem.id_empty
6.8 + [(Problem.prep_input @{theory} "pbl_equ" [] Problem.id_empty
6.9 (["equation"],
6.10 [("#Given" ,["equality e_e", "solveFor v_v"]),
6.11 ("#Where" ,["matches (?a = ?b) e_e"]),
6.12 ("#Find" ,["solutions v_v'i'"])],
6.13 Rule_Set.append_rules "equation_prls" Rule_Set.empty [Rule.Eval ("Prog_Expr.matches", Prog_Expr.eval_matches "")],
6.14 SOME "solve (e_e::bool, v_v)", [])),
6.15 - (Problem.prep_input thy "pbl_equ_univ" [] Problem.id_empty
6.16 + (Problem.prep_input @{theory} "pbl_equ_univ" [] Problem.id_empty
6.17 (["univariate", "equation"],
6.18 [("#Given" ,["equality e_e", "solveFor v_v"]),
6.19 ("#Where" ,["matches (?a = ?b) e_e"]),
6.20 @@ -73,14 +73,14 @@
6.21 | argl2dtss _ = raise ERROR "Equation.ML: wrong argument for argl2dtss";
6.22 \<close>
6.23 setup \<open>KEStore_Elems.add_cas
6.24 - [((Thm.term_of o the o (TermC.parse thy)) "solveTest",
6.25 + [((Thm.term_of o the o (TermC.parse @{theory})) "solveTest",
6.26 (("Test", ["univariate", "equation", "test"], ["no_met"]), argl2dtss)),
6.27 - ((Thm.term_of o the o (TermC.parse thy)) "solve",
6.28 + ((Thm.term_of o the o (TermC.parse @{theory})) "solve",
6.29 (("Isac_Knowledge", ["univariate", "equation"], ["no_met"]), argl2dtss))]\<close>
6.30
6.31
6.32 setup \<open>KEStore_Elems.add_mets
6.33 - [MethodC.prep_input thy "met_equ" [] MethodC.id_empty
6.34 + [MethodC.prep_input @{theory} "met_equ" [] MethodC.id_empty
6.35 (["Equation"], [],
6.36 {rew_ord'="tless_true", rls'=Rule_Set.Empty, calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty, crls = Atools_erls,
6.37 errpats = [], nrls = Rule_Set.empty},
7.1 --- a/src/Tools/isac/Knowledge/Integrate.thy Thu Jun 10 11:54:20 2021 +0200
7.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy Thu Jun 10 12:23:57 2021 +0200
7.3 @@ -330,7 +330,7 @@
7.4
7.5 (** problems **)
7.6 setup \<open>KEStore_Elems.add_pbts
7.7 - [(Problem.prep_input thy "pbl_fun_integ" [] Problem.id_empty
7.8 + [(Problem.prep_input @{theory} "pbl_fun_integ" [] Problem.id_empty
7.9 (["integrate", "function"],
7.10 [("#Given" ,["functionTerm f_f", "integrateBy v_v"]),
7.11 ("#Find" ,["antiDerivative F_F"])],
7.12 @@ -338,7 +338,7 @@
7.13 SOME "Integrate (f_f, v_v)",
7.14 [["diff", "integration"]])),
7.15 (*here "named" is used differently from Differentiation"*)
7.16 - (Problem.prep_input thy "pbl_fun_integ_nam" [] Problem.id_empty
7.17 + (Problem.prep_input @{theory} "pbl_fun_integ_nam" [] Problem.id_empty
7.18 (["named", "integrate", "function"],
7.19 [("#Given" ,["functionTerm f_f", "integrateBy v_v"]),
7.20 ("#Find" ,["antiDerivativeName F_F"])],
7.21 @@ -356,7 +356,7 @@
7.22 in
7.23 (Rewrite_Set_Inst [(''bdv'', v_v)] ''integration'') t_t)"
7.24 setup \<open>KEStore_Elems.add_mets
7.25 - [MethodC.prep_input thy "met_diffint" [] MethodC.id_empty
7.26 + [MethodC.prep_input @{theory} "met_diffint" [] MethodC.id_empty
7.27 (["diff", "integration"],
7.28 [("#Given" ,["functionTerm f_f", "integrateBy v_v"]), ("#Find" ,["antiDerivative F_F"])],
7.29 {rew_ord'="tless_true", rls'=Atools_erls, calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty,
7.30 @@ -374,7 +374,7 @@
7.31 (Rewrite_Set_Inst [(''bdv'', v_v)] ''integration'')
7.32 ) t_t)"
7.33 setup \<open>KEStore_Elems.add_mets
7.34 - [MethodC.prep_input thy "met_diffint_named" [] MethodC.id_empty
7.35 + [MethodC.prep_input @{theory} "met_diffint_named" [] MethodC.id_empty
7.36 (["diff", "integration", "named"],
7.37 [("#Given" ,["functionTerm f_f", "integrateBy v_v"]),
7.38 ("#Find" ,["antiDerivativeName F_F"])],
8.1 --- a/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy Thu Jun 10 11:54:20 2021 +0200
8.2 +++ b/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy Thu Jun 10 12:23:57 2021 +0200
8.3 @@ -46,10 +46,10 @@
8.4 val thy = @{theory};
8.5 \<close>
8.6 setup \<open>KEStore_Elems.add_pbts
8.7 - [(Problem.prep_input thy "pbl_SP" [] Problem.id_empty (["SignalProcessing"], [], Rule_Set.empty, NONE, [])),
8.8 - (Problem.prep_input thy "pbl_SP_Ztrans" [] Problem.id_empty
8.9 + [(Problem.prep_input @{theory} "pbl_SP" [] Problem.id_empty (["SignalProcessing"], [], Rule_Set.empty, NONE, [])),
8.10 + (Problem.prep_input @{theory} "pbl_SP_Ztrans" [] Problem.id_empty
8.11 (["Z_Transform", "SignalProcessing"], [], Rule_Set.empty, NONE, [])),
8.12 - (Problem.prep_input thy "pbl_SP_Ztrans_inv" [] Problem.id_empty
8.13 + (Problem.prep_input @{theory} "pbl_SP_Ztrans_inv" [] Problem.id_empty
8.14 (["Inverse", "Z_Transform", "SignalProcessing"],
8.15 [("#Given" , ["filterExpression X_eq"]),
8.16 ("#Find" ,["stepResponse n_eq"])], \<comment> \<open>TODO: unused, "u [n]" is introduced by rule1..6\<close>
8.17 @@ -57,13 +57,13 @@
8.18 [["SignalProcessing", "Z_Transform", "Inverse"]]))]\<close>
8.19
8.20 subsection \<open>Setup Parent Nodes in Hierarchy of MethodC\<close>
8.21 -ML \<open>val thy = @{theory}; (*latest version of thy required*)\<close>
8.22 +
8.23 setup \<open>KEStore_Elems.add_mets
8.24 - [MethodC.prep_input thy "met_SP" [] MethodC.id_empty
8.25 + [MethodC.prep_input @{theory} "met_SP" [] MethodC.id_empty
8.26 (["SignalProcessing"], [],
8.27 {rew_ord'="tless_true", rls'= Rule_Set.empty, calc = [], srls = Rule_Set.empty, prls = Rule_Set.empty, crls = Rule_Set.empty,
8.28 errpats = [], nrls = Rule_Set.empty}, @{thm refl}),
8.29 - MethodC.prep_input thy "met_SP_Ztrans" [] MethodC.id_empty
8.30 + MethodC.prep_input @{theory} "met_SP_Ztrans" [] MethodC.id_empty
8.31 (["SignalProcessing", "Z_Transform"], [],
8.32 {rew_ord'="tless_true", rls'= Rule_Set.empty, calc = [], srls = Rule_Set.empty, prls = Rule_Set.empty, crls = Rule_Set.empty,
8.33 errpats = [], nrls = Rule_Set.empty}, @{thm refl})]
8.34 @@ -87,7 +87,7 @@
8.35 [BOOL equ, REAL X_z]
8.36 in X) "
8.37 setup \<open>KEStore_Elems.add_mets
8.38 - [MethodC.prep_input thy "met_SP_Ztrans_inv" [] MethodC.id_empty
8.39 + [MethodC.prep_input @{theory} "met_SP_Ztrans_inv" [] MethodC.id_empty
8.40 (["SignalProcessing", "Z_Transform", "Inverse"],
8.41 [("#Given" ,["filterExpression X_eq", "functionName X_z"]),
8.42 ("#Find" ,["stepResponse n_eq"])], \<comment> \<open>TODO: unused, "u [n]" is introduced by rule1..6\<close>
8.43 @@ -115,7 +115,7 @@
8.44 n_eq = (Rewrite_Set ''inverse_z'' ) X_zeq
8.45 in n_eq)"
8.46 setup \<open>KEStore_Elems.add_mets
8.47 - [MethodC.prep_input thy "met_SP_Ztrans_inv_sub" [] MethodC.id_empty
8.48 + [MethodC.prep_input @{theory} "met_SP_Ztrans_inv_sub" [] MethodC.id_empty
8.49 (["SignalProcessing", "Z_Transform", "Inverse_sub"],
8.50 [("#Given" ,["filterExpression X_eq", "functionName X_z"]),
8.51 ("#Find" ,["stepResponse n_eq"])], \<comment> \<open>TODO: unused, "u [n]" is introduced by rule1..6\<close>
9.1 --- a/src/Tools/isac/Knowledge/LinEq.thy Thu Jun 10 11:54:20 2021 +0200
9.2 +++ b/src/Tools/isac/Knowledge/LinEq.thy Thu Jun 10 12:23:57 2021 +0200
9.3 @@ -111,7 +111,7 @@
9.4 (*----------------------------- problem types --------------------------------*)
9.5 (* ---------linear----------- *)
9.6 setup \<open>KEStore_Elems.add_pbts
9.7 - [(Problem.prep_input thy "pbl_equ_univ_lin" [] Problem.id_empty
9.8 + [(Problem.prep_input @{theory} "pbl_equ_univ_lin" [] Problem.id_empty
9.9 (["LINEAR", "univariate", "equation"],
9.10 [("#Given" ,["equality e_e", "solveFor v_v"]),
9.11 ("#Where" ,["HOL.False", (*WN0509 just detected: this pbl can never be used?!?*)
9.12 @@ -124,7 +124,7 @@
9.13
9.14 (*-------------- methods------------------------------------------------------*)
9.15 setup \<open>KEStore_Elems.add_mets
9.16 - [MethodC.prep_input thy "met_eqlin" [] MethodC.id_empty
9.17 + [MethodC.prep_input @{theory} "met_eqlin" [] MethodC.id_empty
9.18 (["LinEq"], [],
9.19 {rew_ord' = "tless_true",rls' = Atools_erls,calc = [], srls = Rule_Set.empty, prls = Rule_Set.empty,
9.20 crls = LinEq_crls, errpats = [], nrls = norm_Poly},
9.21 @@ -148,7 +148,7 @@
9.22 in
9.23 Or_to_List e_e)"
9.24 setup \<open>KEStore_Elems.add_mets
9.25 - [MethodC.prep_input thy "met_eq_lin" [] MethodC.id_empty
9.26 + [MethodC.prep_input @{theory} "met_eq_lin" [] MethodC.id_empty
9.27 (["LinEq", "solve_lineq_equation"],
9.28 [("#Given", ["equality e_e", "solveFor v_v"]),
9.29 ("#Where", ["Not ((lhs e_e) is_polyrat_in v_v)", "((lhs e_e) has_degree_in v_v) = 1"]),
10.1 --- a/src/Tools/isac/Knowledge/LogExp.thy Thu Jun 10 11:54:20 2021 +0200
10.2 +++ b/src/Tools/isac/Knowledge/LogExp.thy Thu Jun 10 12:23:57 2021 +0200
10.3 @@ -21,7 +21,7 @@
10.4 \<close>
10.5 (** problems **)
10.6 setup \<open>KEStore_Elems.add_pbts
10.7 - [(Problem.prep_input thy "pbl_test_equ_univ_log" [] Problem.id_empty
10.8 + [(Problem.prep_input @{theory} "pbl_test_equ_univ_log" [] Problem.id_empty
10.9 (["logarithmic", "univariate", "equation"],
10.10 [("#Given",["equality e_e", "solveFor v_v"]),
10.11 ("#Where",["matches ((?a log ?v_v) = ?b) e_e"]),
10.12 @@ -43,7 +43,7 @@
10.13 in
10.14 [e_e])"
10.15 setup \<open>KEStore_Elems.add_mets
10.16 - [MethodC.prep_input thy "met_equ_log" [] MethodC.id_empty
10.17 + [MethodC.prep_input @{theory} "met_equ_log" [] MethodC.id_empty
10.18 (["Equation", "solve_log"],
10.19 [("#Given" ,["equality e_e", "solveFor v_v"]),
10.20 ("#Where" ,["matches ((?a log ?v_v) = ?b) e_e"]),
11.1 --- a/src/Tools/isac/Knowledge/Poly.thy Thu Jun 10 11:54:20 2021 +0200
11.2 +++ b/src/Tools/isac/Knowledge/Poly.thy Thu Jun 10 12:23:57 2021 +0200
11.3 @@ -1434,7 +1434,7 @@
11.4
11.5 subsection \<open>problems\<close>
11.6 setup \<open>KEStore_Elems.add_pbts
11.7 - [(Problem.prep_input thy "pbl_simp_poly" [] Problem.id_empty
11.8 + [(Problem.prep_input @{theory} "pbl_simp_poly" [] Problem.id_empty
11.9 (["polynomial", "simplification"],
11.10 [("#Given" ,["Term t_t"]),
11.11 ("#Where" ,["t_t is_polyexp"]),
11.12 @@ -1450,7 +1450,7 @@
11.13 where
11.14 "simplify term = ((Rewrite_Set ''norm_Poly'') term)"
11.15 setup \<open>KEStore_Elems.add_mets
11.16 - [MethodC.prep_input thy "met_simp_poly" [] MethodC.id_empty
11.17 + [MethodC.prep_input @{theory} "met_simp_poly" [] MethodC.id_empty
11.18 (["simplification", "for_polynomials"],
11.19 [("#Given" ,["Term t_t"]),
11.20 ("#Where" ,["t_t is_polyexp"]),
12.1 --- a/src/Tools/isac/Knowledge/PolyEq.thy Thu Jun 10 11:54:20 2021 +0200
12.2 +++ b/src/Tools/isac/Knowledge/PolyEq.thy Thu Jun 10 12:23:57 2021 +0200
12.3 @@ -770,7 +770,7 @@
12.4 d4_polyeq_simplify = d4_polyeq_simplify
12.5
12.6 setup \<open>KEStore_Elems.add_pbts
12.7 - [(Problem.prep_input thy "pbl_equ_univ_poly" [] Problem.id_empty
12.8 + [(Problem.prep_input @{theory} "pbl_equ_univ_poly" [] Problem.id_empty
12.9 (["polynomial", "univariate", "equation"],
12.10 [("#Given" ,["equality e_e", "solveFor v_v"]),
12.11 ("#Where" ,["~((e_e::bool) is_ratequation_in (v_v::real))",
12.12 @@ -779,7 +779,7 @@
12.13 ("#Find" ,["solutions v_v'i'"])],
12.14 PolyEq_prls, SOME "solve (e_e::bool, v_v)", [])),
12.15 (*--- d0 ---*)
12.16 - (Problem.prep_input thy "pbl_equ_univ_poly_deg0" [] Problem.id_empty
12.17 + (Problem.prep_input @{theory} "pbl_equ_univ_poly_deg0" [] Problem.id_empty
12.18 (["degree_0", "polynomial", "univariate", "equation"],
12.19 [("#Given" ,["equality e_e", "solveFor v_v"]),
12.20 ("#Where" ,["matches (?a = 0) e_e",
12.21 @@ -788,7 +788,7 @@
12.22 ("#Find" ,["solutions v_v'i'"])],
12.23 PolyEq_prls, SOME "solve (e_e::bool, v_v)", [["PolyEq", "solve_d0_polyeq_equation"]])),
12.24 (*--- d1 ---*)
12.25 - (Problem.prep_input thy "pbl_equ_univ_poly_deg1" [] Problem.id_empty
12.26 + (Problem.prep_input @{theory} "pbl_equ_univ_poly_deg1" [] Problem.id_empty
12.27 (["degree_1", "polynomial", "univariate", "equation"],
12.28 [("#Given" ,["equality e_e", "solveFor v_v"]),
12.29 ("#Where" ,["matches (?a = 0) e_e",
12.30 @@ -797,7 +797,7 @@
12.31 ("#Find" ,["solutions v_v'i'"])],
12.32 PolyEq_prls, SOME "solve (e_e::bool, v_v)", [["PolyEq", "solve_d1_polyeq_equation"]])),
12.33 (*--- d2 ---*)
12.34 - (Problem.prep_input thy "pbl_equ_univ_poly_deg2" [] Problem.id_empty
12.35 + (Problem.prep_input @{theory} "pbl_equ_univ_poly_deg2" [] Problem.id_empty
12.36 (["degree_2", "polynomial", "univariate", "equation"],
12.37 [("#Given" ,["equality e_e", "solveFor v_v"]),
12.38 ("#Where" ,["matches (?a = 0) e_e",
12.39 @@ -805,7 +805,7 @@
12.40 "((lhs e_e) has_degree_in v_v ) = 2"]),
12.41 ("#Find" ,["solutions v_v'i'"])],
12.42 PolyEq_prls, SOME "solve (e_e::bool, v_v)", [["PolyEq", "solve_d2_polyeq_equation"]])),
12.43 - (Problem.prep_input thy "pbl_equ_univ_poly_deg2_sqonly" [] Problem.id_empty
12.44 + (Problem.prep_input @{theory} "pbl_equ_univ_poly_deg2_sqonly" [] Problem.id_empty
12.45 (["sq_only", "degree_2", "polynomial", "univariate", "equation"],
12.46 [("#Given" ,["equality e_e", "solveFor v_v"]),
12.47 ("#Where" ,["matches ( ?a + ?v_ \<up> 2 = 0) e_e | " ^
12.48 @@ -823,7 +823,7 @@
12.49 ("#Find" ,["solutions v_v'i'"])],
12.50 PolyEq_prls, SOME "solve (e_e::bool, v_v)",
12.51 [["PolyEq", "solve_d2_polyeq_sqonly_equation"]])),
12.52 - (Problem.prep_input thy "pbl_equ_univ_poly_deg2_bdvonly" [] Problem.id_empty
12.53 + (Problem.prep_input @{theory} "pbl_equ_univ_poly_deg2_bdvonly" [] Problem.id_empty
12.54 (["bdv_only", "degree_2", "polynomial", "univariate", "equation"],
12.55 [("#Given", ["equality e_e", "solveFor v_v"]),
12.56 ("#Where", ["matches (?a*?v_ + ?v_ \<up> 2 = 0) e_e | " ^
12.57 @@ -835,14 +835,14 @@
12.58 ("#Find", ["solutions v_v'i'"])],
12.59 PolyEq_prls, SOME "solve (e_e::bool, v_v)",
12.60 [["PolyEq", "solve_d2_polyeq_bdvonly_equation"]])),
12.61 - (Problem.prep_input thy "pbl_equ_univ_poly_deg2_pq" [] Problem.id_empty
12.62 + (Problem.prep_input @{theory} "pbl_equ_univ_poly_deg2_pq" [] Problem.id_empty
12.63 (["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
12.64 [("#Given", ["equality e_e", "solveFor v_v"]),
12.65 ("#Where", ["matches (?a + 1*?v_ \<up> 2 = 0) e_e | " ^
12.66 "matches (?a + ?v_ \<up> 2 = 0) e_e"]),
12.67 ("#Find", ["solutions v_v'i'"])],
12.68 PolyEq_prls, SOME "solve (e_e::bool, v_v)", [["PolyEq", "solve_d2_polyeq_pq_equation"]])),
12.69 - (Problem.prep_input thy "pbl_equ_univ_poly_deg2_abc" [] Problem.id_empty
12.70 + (Problem.prep_input @{theory} "pbl_equ_univ_poly_deg2_abc" [] Problem.id_empty
12.71 (["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
12.72 [("#Given", ["equality e_e", "solveFor v_v"]),
12.73 ("#Where", ["matches (?a + ?v_ \<up> 2 = 0) e_e | " ^
12.74 @@ -850,7 +850,7 @@
12.75 ("#Find", ["solutions v_v'i'"])],
12.76 PolyEq_prls, SOME "solve (e_e::bool, v_v)", [["PolyEq", "solve_d2_polyeq_abc_equation"]])),
12.77 (*--- d3 ---*)
12.78 - (Problem.prep_input thy "pbl_equ_univ_poly_deg3" [] Problem.id_empty
12.79 + (Problem.prep_input @{theory} "pbl_equ_univ_poly_deg3" [] Problem.id_empty
12.80 (["degree_3", "polynomial", "univariate", "equation"],
12.81 [("#Given", ["equality e_e", "solveFor v_v"]),
12.82 ("#Where", ["matches (?a = 0) e_e",
12.83 @@ -859,7 +859,7 @@
12.84 ("#Find", ["solutions v_v'i'"])],
12.85 PolyEq_prls, SOME "solve (e_e::bool, v_v)", [["PolyEq", "solve_d3_polyeq_equation"]])),
12.86 (*--- d4 ---*)
12.87 - (Problem.prep_input thy "pbl_equ_univ_poly_deg4" [] Problem.id_empty
12.88 + (Problem.prep_input @{theory} "pbl_equ_univ_poly_deg4" [] Problem.id_empty
12.89 (["degree_4", "polynomial", "univariate", "equation"],
12.90 [("#Given", ["equality e_e", "solveFor v_v"]),
12.91 ("#Where", ["matches (?a = 0) e_e",
12.92 @@ -868,7 +868,7 @@
12.93 ("#Find", ["solutions v_v'i'"])],
12.94 PolyEq_prls, SOME "solve (e_e::bool, v_v)", [(*["PolyEq", "solve_d4_polyeq_equation"]*)])),
12.95 (*--- normalise ---*)
12.96 - (Problem.prep_input thy "pbl_equ_univ_poly_norm" [] Problem.id_empty
12.97 + (Problem.prep_input @{theory} "pbl_equ_univ_poly_norm" [] Problem.id_empty
12.98 (["normalise", "polynomial", "univariate", "equation"],
12.99 [("#Given", ["equality e_e", "solveFor v_v"]),
12.100 ("#Where", ["(Not((matches (?a = 0 ) e_e ))) |" ^
12.101 @@ -876,7 +876,7 @@
12.102 ("#Find", ["solutions v_v'i'"])],
12.103 PolyEq_prls, SOME "solve (e_e::bool, v_v)", [["PolyEq", "normalise_poly"]])),
12.104 (*-------------------------expanded-----------------------*)
12.105 - (Problem.prep_input thy "pbl_equ_univ_expand" [] Problem.id_empty
12.106 + (Problem.prep_input @{theory} "pbl_equ_univ_expand" [] Problem.id_empty
12.107 (["expanded", "univariate", "equation"],
12.108 [("#Given", ["equality e_e", "solveFor v_v"]),
12.109 ("#Where", ["matches (?a = 0) e_e",
12.110 @@ -884,7 +884,7 @@
12.111 ("#Find", ["solutions v_v'i'"])],
12.112 PolyEq_prls, SOME "solve (e_e::bool, v_v)", [])),
12.113 (*--- d2 ---*)
12.114 - (Problem.prep_input thy "pbl_equ_univ_expand_deg2" [] Problem.id_empty
12.115 + (Problem.prep_input @{theory} "pbl_equ_univ_expand_deg2" [] Problem.id_empty
12.116 (["degree_2", "expanded", "univariate", "equation"],
12.117 [("#Given", ["equality e_e", "solveFor v_v"]),
12.118 ("#Where", ["((lhs e_e) has_degree_in v_v) = 2"]),
12.119 @@ -893,7 +893,7 @@
12.120
12.121 text \<open>"-------------------------methods-----------------------"\<close>
12.122 setup \<open>KEStore_Elems.add_mets
12.123 - [MethodC.prep_input thy "met_polyeq" [] MethodC.id_empty
12.124 + [MethodC.prep_input @{theory} "met_polyeq" [] MethodC.id_empty
12.125 (["PolyEq"], [],
12.126 {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty,
12.127 crls=PolyEq_crls, errpats = [], nrls = norm_Rational},
12.128 @@ -914,7 +914,7 @@
12.129 SubProblem (''PolyEq'', [''polynomial'', ''univariate'', ''equation''], [''no_met''])
12.130 [BOOL e_e, REAL v_v])"
12.131 setup \<open>KEStore_Elems.add_mets
12.132 - [MethodC.prep_input thy "met_polyeq_norm" [] MethodC.id_empty
12.133 + [MethodC.prep_input @{theory} "met_polyeq_norm" [] MethodC.id_empty
12.134 (["PolyEq", "normalise_poly"],
12.135 [("#Given" ,["equality e_e", "solveFor v_v"]),
12.136 ("#Where" ,["(Not((matches (?a = 0 ) e_e ))) | (Not(((lhs e_e) is_poly_in v_v)))"]),
12.137 @@ -932,7 +932,7 @@
12.138 in
12.139 Or_to_List e_e)"
12.140 setup \<open>KEStore_Elems.add_mets
12.141 - [MethodC.prep_input thy "met_polyeq_d0" [] MethodC.id_empty
12.142 + [MethodC.prep_input @{theory} "met_polyeq_d0" [] MethodC.id_empty
12.143 (["PolyEq", "solve_d0_polyeq_equation"],
12.144 [("#Given" ,["equality e_e", "solveFor v_v"]),
12.145 ("#Where" ,["(lhs e_e) is_poly_in v_v ", "((lhs e_e) has_degree_in v_v) = 0"]),
12.146 @@ -955,7 +955,7 @@
12.147 in
12.148 Check_elementwise L_L {(v_v::real). Assumptions})"
12.149 setup \<open>KEStore_Elems.add_mets
12.150 - [MethodC.prep_input thy "met_polyeq_d1" [] MethodC.id_empty
12.151 + [MethodC.prep_input @{theory} "met_polyeq_d1" [] MethodC.id_empty
12.152 (["PolyEq", "solve_d1_polyeq_equation"],
12.153 [("#Given" ,["equality e_e", "solveFor v_v"]),
12.154 ("#Where" ,["(lhs e_e) is_poly_in v_v ", "((lhs e_e) has_degree_in v_v) = 1"]),
12.155 @@ -980,7 +980,7 @@
12.156 in
12.157 Check_elementwise L_L {(v_v::real). Assumptions})"
12.158 setup \<open>KEStore_Elems.add_mets
12.159 - [MethodC.prep_input thy "met_polyeq_d22" [] MethodC.id_empty
12.160 + [MethodC.prep_input @{theory} "met_polyeq_d22" [] MethodC.id_empty
12.161 (["PolyEq", "solve_d2_polyeq_equation"],
12.162 [("#Given" ,["equality e_e", "solveFor v_v"]),
12.163 ("#Where" ,["(lhs e_e) is_poly_in v_v ", "((lhs e_e) has_degree_in v_v) = 2"]),
12.164 @@ -1005,7 +1005,7 @@
12.165 in
12.166 Check_elementwise L_L {(v_v::real). Assumptions})"
12.167 setup \<open>KEStore_Elems.add_mets
12.168 - [MethodC.prep_input thy "met_polyeq_d2_bdvonly" [] MethodC.id_empty
12.169 + [MethodC.prep_input @{theory} "met_polyeq_d2_bdvonly" [] MethodC.id_empty
12.170 (["PolyEq", "solve_d2_polyeq_bdvonly_equation"],
12.171 [("#Given" ,["equality e_e", "solveFor v_v"]),
12.172 ("#Where" ,["(lhs e_e) is_poly_in v_v ", "((lhs e_e) has_degree_in v_v) = 2"]),
12.173 @@ -1028,7 +1028,7 @@
12.174 in
12.175 Check_elementwise L_L {(v_v::real). Assumptions})"
12.176 setup \<open>KEStore_Elems.add_mets
12.177 - [MethodC.prep_input thy "met_polyeq_d2_sqonly" [] MethodC.id_empty
12.178 + [MethodC.prep_input @{theory} "met_polyeq_d2_sqonly" [] MethodC.id_empty
12.179 (["PolyEq", "solve_d2_polyeq_sqonly_equation"],
12.180 [("#Given" ,["equality e_e", "solveFor v_v"]),
12.181 ("#Where" ,["(lhs e_e) is_poly_in v_v ", "((lhs e_e) has_degree_in v_v) = 2"]),
12.182 @@ -1051,7 +1051,7 @@
12.183 in
12.184 Check_elementwise L_L {(v_v::real). Assumptions})"
12.185 setup \<open>KEStore_Elems.add_mets
12.186 - [MethodC.prep_input thy "met_polyeq_d2_pq" [] MethodC.id_empty
12.187 + [MethodC.prep_input @{theory} "met_polyeq_d2_pq" [] MethodC.id_empty
12.188 (["PolyEq", "solve_d2_polyeq_pq_equation"],
12.189 [("#Given" ,["equality e_e", "solveFor v_v"]),
12.190 ("#Where" ,["(lhs e_e) is_poly_in v_v ", "((lhs e_e) has_degree_in v_v) = 2"]),
12.191 @@ -1073,7 +1073,7 @@
12.192 L_L = Or_to_List e_e
12.193 in Check_elementwise L_L {(v_v::real). Assumptions})"
12.194 setup \<open>KEStore_Elems.add_mets
12.195 - [MethodC.prep_input thy "met_polyeq_d2_abc" [] MethodC.id_empty
12.196 + [MethodC.prep_input @{theory} "met_polyeq_d2_abc" [] MethodC.id_empty
12.197 (["PolyEq", "solve_d2_polyeq_abc_equation"],
12.198 [("#Given" ,["equality e_e", "solveFor v_v"]),
12.199 ("#Where" ,["(lhs e_e) is_poly_in v_v ", "((lhs e_e) has_degree_in v_v) = 2"]),
12.200 @@ -1100,7 +1100,7 @@
12.201 in
12.202 Check_elementwise L_L {(v_v::real). Assumptions})"
12.203 setup \<open>KEStore_Elems.add_mets
12.204 - [MethodC.prep_input thy "met_polyeq_d3" [] MethodC.id_empty
12.205 + [MethodC.prep_input @{theory} "met_polyeq_d3" [] MethodC.id_empty
12.206 (["PolyEq", "solve_d3_polyeq_equation"],
12.207 [("#Given" ,["equality e_e", "solveFor v_v"]),
12.208 ("#Where" ,["(lhs e_e) is_poly_in v_v ", "((lhs e_e) has_degree_in v_v) = 3"]),
12.209 @@ -1130,7 +1130,7 @@
12.210 in
12.211 Or_to_List e_e)"
12.212 setup \<open>KEStore_Elems.add_mets
12.213 - [MethodC.prep_input thy "met_polyeq_complsq" [] MethodC.id_empty
12.214 + [MethodC.prep_input @{theory} "met_polyeq_complsq" [] MethodC.id_empty
12.215 (["PolyEq", "complete_square"],
12.216 [("#Given" ,["equality e_e", "solveFor v_v"]),
12.217 ("#Where" ,["matches (?a = 0) e_e", "((lhs e_e) has_degree_in v_v) = 2"]),
13.1 --- a/src/Tools/isac/Knowledge/PolyMinus.thy Thu Jun 10 11:54:20 2021 +0200
13.2 +++ b/src/Tools/isac/Knowledge/PolyMinus.thy Thu Jun 10 12:23:57 2021 +0200
13.3 @@ -399,9 +399,9 @@
13.4
13.5 (** problems **)
13.6 setup \<open>KEStore_Elems.add_pbts
13.7 - [(Problem.prep_input thy "pbl_vereinf_poly" [] Problem.id_empty
13.8 + [(Problem.prep_input @{theory} "pbl_vereinf_poly" [] Problem.id_empty
13.9 (["polynom", "vereinfachen"], [], Rule_Set.Empty, NONE, [])),
13.10 - (Problem.prep_input thy "pbl_vereinf_poly_minus" [] Problem.id_empty
13.11 + (Problem.prep_input @{theory} "pbl_vereinf_poly_minus" [] Problem.id_empty
13.12 (["plus_minus", "polynom", "vereinfachen"],
13.13 [("#Given", ["Term t_t"]),
13.14 ("#Where", ["t_t is_polyexp",
13.15 @@ -426,7 +426,7 @@
13.16 Rule.Thm ("not_false",ThmC.numerals_to_Free @{thm not_false})
13.17 (*"(~ False) = True"*)],
13.18 SOME "Vereinfache t_t", [["simplification", "for_polynomials", "with_minus"]])),
13.19 - (Problem.prep_input thy "pbl_vereinf_poly_klammer" [] Problem.id_empty
13.20 + (Problem.prep_input @{theory} "pbl_vereinf_poly_klammer" [] Problem.id_empty
13.21 (["klammer", "polynom", "vereinfachen"],
13.22 [("#Given" ,["Term t_t"]),
13.23 ("#Where" ,["t_t is_polyexp",
13.24 @@ -448,7 +448,7 @@
13.25 (*"(~ False) = True"*)],
13.26 SOME "Vereinfache t_t",
13.27 [["simplification", "for_polynomials", "with_parentheses"]])),
13.28 - (Problem.prep_input thy "pbl_vereinf_poly_klammer_mal" [] Problem.id_empty
13.29 + (Problem.prep_input @{theory} "pbl_vereinf_poly_klammer_mal" [] Problem.id_empty
13.30 (["binom_klammer", "polynom", "vereinfachen"],
13.31 [("#Given", ["Term t_t"]),
13.32 ("#Where", ["t_t is_polyexp"]),
13.33 @@ -457,8 +457,8 @@
13.34 Rule.Eval ("Poly.is_polyexp", eval_is_polyexp "")],
13.35 SOME "Vereinfache t_t",
13.36 [["simplification", "for_polynomials", "with_parentheses_mult"]])),
13.37 - (Problem.prep_input thy "pbl_probe" [] Problem.id_empty (["probe"], [], Rule_Set.Empty, NONE, [])),
13.38 - (Problem.prep_input thy "pbl_probe_poly" [] Problem.id_empty
13.39 + (Problem.prep_input @{theory} "pbl_probe" [] Problem.id_empty (["probe"], [], Rule_Set.Empty, NONE, [])),
13.40 + (Problem.prep_input @{theory} "pbl_probe_poly" [] Problem.id_empty
13.41 (["polynom", "probe"],
13.42 [("#Given", ["Pruefe e_e", "mitWert w_w"]),
13.43 ("#Where", ["e_e is_polyexp"]),
13.44 @@ -467,7 +467,7 @@
13.45 Rule.Eval ("Poly.is_polyexp", eval_is_polyexp "")],
13.46 SOME "Probe e_e w_w",
13.47 [["probe", "fuer_polynom"]])),
13.48 - (Problem.prep_input thy "pbl_probe_bruch" [] Problem.id_empty
13.49 + (Problem.prep_input @{theory} "pbl_probe_bruch" [] Problem.id_empty
13.50 (["bruch", "probe"],
13.51 [("#Given" ,["Pruefe e_e", "mitWert w_w"]),
13.52 ("#Where" ,["e_e is_ratpolyexp"]),
13.53 @@ -487,7 +487,7 @@
13.54 (Try (Rewrite_Set ''verschoenere'')))
13.55 ) t_t)"
13.56 setup \<open>KEStore_Elems.add_mets
13.57 - [MethodC.prep_input thy "met_simp_poly_minus" [] MethodC.id_empty
13.58 + [MethodC.prep_input @{theory} "met_simp_poly_minus" [] MethodC.id_empty
13.59 (["simplification", "for_polynomials", "with_minus"],
13.60 [("#Given" ,["Term t_t"]),
13.61 ("#Where" ,["t_t is_polyexp",
13.62 @@ -522,7 +522,7 @@
13.63 (Try (Rewrite_Set ''verschoenere'')))
13.64 ) t_t)"
13.65 setup \<open>KEStore_Elems.add_mets
13.66 - [MethodC.prep_input thy "met_simp_poly_parenth" [] MethodC.id_empty
13.67 + [MethodC.prep_input @{theory} "met_simp_poly_parenth" [] MethodC.id_empty
13.68 (["simplification", "for_polynomials", "with_parentheses"],
13.69 [("#Given" ,["Term t_t"]),
13.70 ("#Where" ,["t_t is_polyexp"]),
13.71 @@ -547,7 +547,7 @@
13.72 (Try (Rewrite_Set ''verschoenere'')))
13.73 ) t_t)"
13.74 setup \<open>KEStore_Elems.add_mets
13.75 - [MethodC.prep_input thy "met_simp_poly_parenth_mult" [] MethodC.id_empty
13.76 + [MethodC.prep_input @{theory} "met_simp_poly_parenth_mult" [] MethodC.id_empty
13.77 (["simplification", "for_polynomials", "with_parentheses_mult"],
13.78 [("#Given" ,["Term t_t"]), ("#Where" ,["t_t is_polyexp"]), ("#Find" ,["normalform n_n"])],
13.79 {rew_ord'="tless_true", rls' = Rule_Set.empty, calc = [], srls = Rule_Set.empty,
13.80 @@ -557,7 +557,7 @@
13.81 @{thm simplify3.simps})]
13.82 \<close>
13.83 setup \<open>KEStore_Elems.add_mets
13.84 - [MethodC.prep_input thy "met_probe" [] MethodC.id_empty
13.85 + [MethodC.prep_input @{theory} "met_probe" [] MethodC.id_empty
13.86 (["probe"], [],
13.87 {rew_ord'="tless_true", rls' = Rule_Set.empty, calc = [], srls = Rule_Set.empty, prls = Rule_Set.Empty, crls = Rule_Set.empty,
13.88 errpats = [], nrls = Rule_Set.Empty},
13.89 @@ -577,7 +577,7 @@
13.90 (Try (Repeat (Calculate ''MINUS''))))
13.91 ) e_e)"
13.92 setup \<open>KEStore_Elems.add_mets
13.93 - [MethodC.prep_input thy "met_probe_poly" [] MethodC.id_empty
13.94 + [MethodC.prep_input @{theory} "met_probe_poly" [] MethodC.id_empty
13.95 (["probe", "fuer_polynom"],
13.96 [("#Given" ,["Pruefe e_e", "mitWert w_w"]),
13.97 ("#Where" ,["e_e is_polyexp"]),
13.98 @@ -589,7 +589,7 @@
13.99 @{thm mache_probe.simps})]
13.100 \<close>
13.101 setup \<open>KEStore_Elems.add_mets
13.102 - [MethodC.prep_input thy "met_probe_bruch" [] MethodC.id_empty
13.103 + [MethodC.prep_input @{theory} "met_probe_bruch" [] MethodC.id_empty
13.104 (["probe", "fuer_bruch"],
13.105 [("#Given" ,["Pruefe e_e", "mitWert w_w"]),
13.106 ("#Where" ,["e_e is_ratpolyexp"]),
14.1 --- a/src/Tools/isac/Knowledge/RatEq.thy Thu Jun 10 11:54:20 2021 +0200
14.2 +++ b/src/Tools/isac/Knowledge/RatEq.thy Thu Jun 10 12:23:57 2021 +0200
14.3 @@ -161,7 +161,7 @@
14.4
14.5 subsection \<open>problems\<close>
14.6 setup \<open>KEStore_Elems.add_pbts
14.7 - [(Problem.prep_input thy "pbl_equ_univ_rat" [] Problem.id_empty
14.8 + [(Problem.prep_input @{theory} "pbl_equ_univ_rat" [] Problem.id_empty
14.9 (["rational", "univariate", "equation"],
14.10 [("#Given", ["equality e_e", "solveFor v_v"]),
14.11 ("#Where", ["(e_e::bool) is_ratequation_in (v_v::real)"]),
14.12 @@ -170,7 +170,7 @@
14.13
14.14 subsection \<open>methods\<close>
14.15 setup \<open>KEStore_Elems.add_mets
14.16 - [MethodC.prep_input thy "met_rateq" [] MethodC.id_empty
14.17 + [MethodC.prep_input @{theory} "met_rateq" [] MethodC.id_empty
14.18 (["RatEq"], [],
14.19 {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty,
14.20 crls=RatEq_crls, errpats = [], nrls = norm_Rational}, @{thm refl})]\<close>
14.21 @@ -188,7 +188,7 @@
14.22 in
14.23 Check_elementwise L_L {(v_v::real). Assumptions})"
14.24 setup \<open>KEStore_Elems.add_mets
14.25 - [MethodC.prep_input thy "met_rat_eq" [] MethodC.id_empty
14.26 + [MethodC.prep_input @{theory} "met_rat_eq" [] MethodC.id_empty
14.27 (["RatEq", "solve_rat_equation"],
14.28 [("#Given" ,["equality e_e", "solveFor v_v"]),
14.29 ("#Where" ,["(e_e::bool) is_ratequation_in (v_v::real)"]),
15.1 --- a/src/Tools/isac/Knowledge/Rational.thy Thu Jun 10 11:54:20 2021 +0200
15.2 +++ b/src/Tools/isac/Knowledge/Rational.thy Thu Jun 10 12:23:57 2021 +0200
15.3 @@ -878,7 +878,7 @@
15.4
15.5 section \<open>A problem for simplification of rationals\<close>
15.6 setup \<open>KEStore_Elems.add_pbts
15.7 - [(Problem.prep_input thy "pbl_simp_rat" [] Problem.id_empty
15.8 + [(Problem.prep_input @{theory} "pbl_simp_rat" [] Problem.id_empty
15.9 (["rational", "simplification"],
15.10 [("#Given" ,["Term t_t"]),
15.11 ("#Where" ,["t_t is_ratpolyexp"]),
15.12 @@ -906,7 +906,7 @@
15.13 Try (Rewrite_Set ''discard_parentheses1''))
15.14 term)"
15.15 setup \<open>KEStore_Elems.add_mets
15.16 - [MethodC.prep_input thy "met_simp_rat" [] MethodC.id_empty
15.17 + [MethodC.prep_input @{theory} "met_simp_rat" [] MethodC.id_empty
15.18 (["simplification", "of_rationals"],
15.19 [("#Given" ,["Term t_t"]),
15.20 ("#Where" ,["t_t is_ratpolyexp"]),
16.1 --- a/src/Tools/isac/Knowledge/RootEq.thy Thu Jun 10 11:54:20 2021 +0200
16.2 +++ b/src/Tools/isac/Knowledge/RootEq.thy Thu Jun 10 12:23:57 2021 +0200
16.3 @@ -445,7 +445,7 @@
16.4 (*Ambiguous input produces 5 parse trees -----------------------------------------------------\\*)
16.5 setup \<open>KEStore_Elems.add_pbts
16.6 (* ---------root----------- *)
16.7 - [(Problem.prep_input thy "pbl_equ_univ_root" [] Problem.id_empty
16.8 + [(Problem.prep_input @{theory} "pbl_equ_univ_root" [] Problem.id_empty
16.9 (["rootX", "univariate", "equation"],
16.10 [("#Given" ,["equality e_e", "solveFor v_v"]),
16.11 ("#Where" ,["(lhs e_e) is_rootTerm_in (v_v::real) | " ^
16.12 @@ -453,7 +453,7 @@
16.13 ("#Find" ,["solutions v_v'i'"])],
16.14 RootEq_prls, SOME "solve (e_e::bool, v_v)", [])),
16.15 (* ---------sqrt----------- *)
16.16 - (Problem.prep_input thy "pbl_equ_univ_root_sq" [] Problem.id_empty
16.17 + (Problem.prep_input @{theory} "pbl_equ_univ_root_sq" [] Problem.id_empty
16.18 (["sq", "rootX", "univariate", "equation"],
16.19 [("#Given" ,["equality e_e", "solveFor v_v"]),
16.20 ("#Where" ,["( ((lhs e_e) is_sqrtTerm_in (v_v::real)) &" ^
16.21 @@ -463,7 +463,7 @@
16.22 ("#Find" ,["solutions v_v'i'"])],
16.23 RootEq_prls, SOME "solve (e_e::bool, v_v)", [["RootEq", "solve_sq_root_equation"]])),
16.24 (* ---------normalise----------- *)
16.25 - (Problem.prep_input thy "pbl_equ_univ_root_norm" [] Problem.id_empty
16.26 + (Problem.prep_input @{theory} "pbl_equ_univ_root_norm" [] Problem.id_empty
16.27 (["normalise", "rootX", "univariate", "equation"],
16.28 [("#Given" ,["equality e_e", "solveFor v_v"]),
16.29 ("#Where" ,["( ((lhs e_e) is_sqrtTerm_in (v_v::real)) &" ^
16.30 @@ -476,7 +476,7 @@
16.31
16.32 subsection \<open>methods\<close>
16.33 setup \<open>KEStore_Elems.add_mets
16.34 - [MethodC.prep_input thy "met_rooteq" [] MethodC.id_empty
16.35 + [MethodC.prep_input @{theory} "met_rooteq" [] MethodC.id_empty
16.36 (["RootEq"], [],
16.37 {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty,
16.38 crls=RootEq_crls, errpats = [], nrls = norm_Poly}, @{thm refl})]
16.39 @@ -497,7 +497,7 @@
16.40 SubProblem (''RootEq'', [''univariate'', ''equation''], [''no_met''])
16.41 [BOOL e_e, REAL v_v])"
16.42 setup \<open>KEStore_Elems.add_mets
16.43 - [MethodC.prep_input thy "met_rooteq_norm" [] MethodC.id_empty
16.44 + [MethodC.prep_input @{theory} "met_rooteq_norm" [] MethodC.id_empty
16.45 (["RootEq", "norm_sq_root_equation"],
16.46 [("#Given" ,["equality e_e", "solveFor v_v"]),
16.47 ("#Where" ,["( ((lhs e_e) is_sqrtTerm_in (v_v::real)) &" ^
16.48 @@ -530,7 +530,7 @@
16.49 [BOOL e_e, REAL v_v])
16.50 in Check_elementwise L_L {(v_v::real). Assumptions})"
16.51 setup \<open>KEStore_Elems.add_mets
16.52 - [MethodC.prep_input thy "met_rooteq_sq" [] MethodC.id_empty
16.53 + [MethodC.prep_input @{theory} "met_rooteq_sq" [] MethodC.id_empty
16.54 (["RootEq", "solve_sq_root_equation"],
16.55 [("#Given" ,["equality e_e", "solveFor v_v"]),
16.56 ("#Where" ,["(((lhs e_e) is_sqrtTerm_in (v_v::real)) & " ^
16.57 @@ -562,7 +562,7 @@
16.58 SubProblem (''RootEq'',[''univariate'', ''equation''], [''no_met''])
16.59 [BOOL e_e, REAL v_v])"
16.60 setup \<open>KEStore_Elems.add_mets
16.61 - [MethodC.prep_input thy "met_rooteq_sq_right" [] MethodC.id_empty
16.62 + [MethodC.prep_input @{theory} "met_rooteq_sq_right" [] MethodC.id_empty
16.63 (["RootEq", "solve_right_sq_root_equation"],
16.64 [("#Given" ,["equality e_e", "solveFor v_v"]),
16.65 ("#Where" ,["(rhs e_e) is_sqrtTerm_in v_v"]),
16.66 @@ -591,7 +591,7 @@
16.67 SubProblem (''RootEq'',[''univariate'',''equation''], [''no_met''])
16.68 [BOOL e_e, REAL v_v])"
16.69 setup \<open>KEStore_Elems.add_mets
16.70 - [MethodC.prep_input thy "met_rooteq_sq_left" [] MethodC.id_empty
16.71 + [MethodC.prep_input @{theory} "met_rooteq_sq_left" [] MethodC.id_empty
16.72 (["RootEq", "solve_left_sq_root_equation"],
16.73 [("#Given" ,["equality e_e", "solveFor v_v"]),
16.74 ("#Where" ,["(lhs e_e) is_sqrtTerm_in v_v"]),
17.1 --- a/src/Tools/isac/Knowledge/RootRatEq.thy Thu Jun 10 11:54:20 2021 +0200
17.2 +++ b/src/Tools/isac/Knowledge/RootRatEq.thy Thu Jun 10 12:23:57 2021 +0200
17.3 @@ -123,7 +123,7 @@
17.4 subsection \<open>problems\<close>
17.5
17.6 setup \<open>KEStore_Elems.add_pbts
17.7 - [(Problem.prep_input thy "pbl_equ_univ_root_sq_rat" [] Problem.id_empty
17.8 + [(Problem.prep_input @{theory} "pbl_equ_univ_root_sq_rat" [] Problem.id_empty
17.9 (["rat", "sq", "rootX", "univariate", "equation"],
17.10 [("#Given" ,["equality e_e", "solveFor v_v"]),
17.11 ("#Where" ,["( (lhs e_e) is_rootRatAddTerm_in (v_v::real) )| " ^
17.12 @@ -151,7 +151,7 @@
17.13 (Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''rootrat_solve'')) ) e_e
17.14 in SubProblem (''RootEq'', [''univariate'', ''equation''], [''no_met'']) [BOOL e_e, REAL v_v])"
17.15 setup \<open>KEStore_Elems.add_mets
17.16 - [MethodC.prep_input thy "met_rootrateq_elim" [] MethodC.id_empty
17.17 + [MethodC.prep_input @{theory} "met_rootrateq_elim" [] MethodC.id_empty
17.18 (["RootRatEq", "elim_rootrat_equation"],
17.19 [("#Given" ,["equality e_e", "solveFor v_v"]),
17.20 ("#Where" ,["( (lhs e_e) is_rootRatAddTerm_in (v_v::real) ) | " ^
18.1 --- a/src/Tools/isac/Knowledge/Simplify.thy Thu Jun 10 11:54:20 2021 +0200
18.2 +++ b/src/Tools/isac/Knowledge/Simplify.thy Thu Jun 10 12:23:57 2021 +0200
18.3 @@ -25,12 +25,12 @@
18.4 \<close>
18.5 (** problems **)
18.6 setup \<open>KEStore_Elems.add_pbts
18.7 - [(Problem.prep_input thy "pbl_simp" [] Problem.id_empty
18.8 + [(Problem.prep_input @{theory} "pbl_simp" [] Problem.id_empty
18.9 (["simplification"],
18.10 [("#Given" ,["Term t_t"]),
18.11 ("#Find" ,["normalform n_n"])],
18.12 Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)], SOME "Simplify t_t", [])),
18.13 - (Problem.prep_input thy "pbl_vereinfache" [] Problem.id_empty
18.14 + (Problem.prep_input @{theory} "pbl_vereinfache" [] Problem.id_empty
18.15 (["vereinfachen"],
18.16 [("#Given", ["Term t_t"]),
18.17 ("#Find", ["normalform n_n"])],
18.18 @@ -38,7 +38,7 @@
18.19
18.20 (** methods **)
18.21 setup \<open>KEStore_Elems.add_mets
18.22 - [MethodC.prep_input thy "met_tsimp" [] MethodC.id_empty
18.23 + [MethodC.prep_input @{theory} "met_tsimp" [] MethodC.id_empty
18.24 (["simplification"],
18.25 [("#Given" ,["Term t_t"]),
18.26 ("#Find" ,["normalform n_n"])],
18.27 @@ -58,16 +58,16 @@
18.28 "Simplify (2*a + 3*a)");
18.29 *)
18.30 fun argl2dtss t =
18.31 - [((Thm.term_of o the o (TermC.parse thy)) "Term", t),
18.32 - ((Thm.term_of o the o (TermC.parse thy)) "normalform",
18.33 - [(Thm.term_of o the o (TermC.parse thy)) "N"])
18.34 + [((Thm.term_of o the o (TermC.parse @{theory})) "Term", t),
18.35 + ((Thm.term_of o the o (TermC.parse @{theory})) "normalform",
18.36 + [(Thm.term_of o the o (TermC.parse @{theory})) "N"])
18.37 ]
18.38 (*| argl2dtss _ = raise ERROR "Simplify.ML: wrong argument for argl2dtss"*);
18.39 \<close>
18.40 setup \<open>KEStore_Elems.add_cas
18.41 - [((Thm.term_of o the o (TermC.parse thy)) "Simplify",
18.42 + [((Thm.term_of o the o (TermC.parse @{theory})) "Simplify",
18.43 (("Isac_Knowledge", ["simplification"], ["no_met"]), argl2dtss)),
18.44 - ((Thm.term_of o the o (TermC.parse thy)) "Vereinfache",
18.45 + ((Thm.term_of o the o (TermC.parse @{theory})) "Vereinfache",
18.46 (("Isac_Knowledge", ["vereinfachen"], ["no_met"]), argl2dtss))]\<close>
18.47
18.48 ML \<open>
19.1 --- a/src/Tools/isac/Knowledge/Test.thy Thu Jun 10 11:54:20 2021 +0200
19.2 +++ b/src/Tools/isac/Knowledge/Test.thy Thu Jun 10 12:23:57 2021 +0200
19.3 @@ -574,20 +574,20 @@
19.4 subsection \<open>problems\<close>
19.5 (** problem types **)
19.6 setup \<open>KEStore_Elems.add_pbts
19.7 - [(Problem.prep_input thy "pbl_test" [] Problem.id_empty (["test"], [], Rule_Set.empty, NONE, [])),
19.8 - (Problem.prep_input thy "pbl_test_equ" [] Problem.id_empty
19.9 + [(Problem.prep_input @{theory} "pbl_test" [] Problem.id_empty (["test"], [], Rule_Set.empty, NONE, [])),
19.10 + (Problem.prep_input @{theory} "pbl_test_equ" [] Problem.id_empty
19.11 (["equation", "test"],
19.12 [("#Given" ,["equality e_e", "solveFor v_v"]),
19.13 ("#Where" ,["matches (?a = ?b) e_e"]),
19.14 ("#Find" ,["solutions v_v'i'"])],
19.15 assoc_rls' @{theory} "matches", SOME "solve (e_e::bool, v_v)", [])),
19.16 - (Problem.prep_input thy "pbl_test_uni" [] Problem.id_empty
19.17 + (Problem.prep_input @{theory} "pbl_test_uni" [] Problem.id_empty
19.18 (["univariate", "equation", "test"],
19.19 [("#Given" ,["equality e_e", "solveFor v_v"]),
19.20 ("#Where" ,["matches (?a = ?b) e_e"]),
19.21 ("#Find" ,["solutions v_v'i'"])],
19.22 assoc_rls' @{theory} "matches", SOME "solve (e_e::bool, v_v)", [])),
19.23 - (Problem.prep_input thy "pbl_test_uni_lin" [] Problem.id_empty
19.24 + (Problem.prep_input @{theory} "pbl_test_uni_lin" [] Problem.id_empty
19.25 (["LINEAR", "univariate", "equation", "test"],
19.26 [("#Given" ,["equality e_e", "solveFor v_v"]),
19.27 ("#Where" ,["(matches ( v_v = 0) e_e) | (matches ( ?b*v_v = 0) e_e) |" ^
19.28 @@ -776,7 +776,7 @@
19.29
19.30 section \<open>problems\<close>
19.31 setup \<open>KEStore_Elems.add_pbts
19.32 - [(Problem.prep_input thy "pbl_test_uni_plain2" [] Problem.id_empty
19.33 + [(Problem.prep_input @{theory} "pbl_test_uni_plain2" [] Problem.id_empty
19.34 (["plain_square", "univariate", "equation", "test"],
19.35 [("#Given" ,["equality e_e", "solveFor v_v"]),
19.36 ("#Where" ,["(matches (?a + ?b*v_v \<up> 2 = 0) e_e) |" ^
19.37 @@ -786,28 +786,28 @@
19.38 ("#Find" ,["solutions v_v'i'"])],
19.39 assoc_rls' @{theory} "matches",
19.40 SOME "solve (e_e::bool, v_v)", [["Test", "solve_plain_square"]])),
19.41 - (Problem.prep_input thy "pbl_test_uni_poly" [] Problem.id_empty
19.42 + (Problem.prep_input @{theory} "pbl_test_uni_poly" [] Problem.id_empty
19.43 (["polynomial", "univariate", "equation", "test"],
19.44 [("#Given" ,["equality (v_v \<up> 2 + p_p * v_v + q__q = 0)", "solveFor v_v"]),
19.45 ("#Where" ,["HOL.False"]),
19.46 ("#Find" ,["solutions v_v'i'"])],
19.47 Rule_Set.empty, SOME "solve (e_e::bool, v_v)", [])),
19.48 - (Problem.prep_input thy "pbl_test_uni_poly_deg2" [] Problem.id_empty
19.49 + (Problem.prep_input @{theory} "pbl_test_uni_poly_deg2" [] Problem.id_empty
19.50 (["degree_two", "polynomial", "univariate", "equation", "test"],
19.51 [("#Given" ,["equality (v_v \<up> 2 + p_p * v_v + q__q = 0)", "solveFor v_v"]),
19.52 ("#Find" ,["solutions v_v'i'"])],
19.53 Rule_Set.empty, SOME "solve (v_v \<up> 2 + p_p * v_v + q__q = 0, v_v)", [])),
19.54 - (Problem.prep_input thy "pbl_test_uni_poly_deg2_pq" [] Problem.id_empty
19.55 + (Problem.prep_input @{theory} "pbl_test_uni_poly_deg2_pq" [] Problem.id_empty
19.56 (["pq_formula", "degree_two", "polynomial", "univariate", "equation", "test"],
19.57 [("#Given" ,["equality (v_v \<up> 2 + p_p * v_v + q__q = 0)", "solveFor v_v"]),
19.58 ("#Find" ,["solutions v_v'i'"])],
19.59 Rule_Set.empty, SOME "solve (v_v \<up> 2 + p_p * v_v + q__q = 0, v_v)", [])),
19.60 - (Problem.prep_input thy "pbl_test_uni_poly_deg2_abc" [] Problem.id_empty
19.61 + (Problem.prep_input @{theory} "pbl_test_uni_poly_deg2_abc" [] Problem.id_empty
19.62 (["abc_formula", "degree_two", "polynomial", "univariate", "equation", "test"],
19.63 [("#Given" ,["equality (a_a * x \<up> 2 + b_b * x + c_c = 0)", "solveFor v_v"]),
19.64 ("#Find" ,["solutions v_v'i'"])],
19.65 Rule_Set.empty, SOME "solve (a_a * x \<up> 2 + b_b * x + c_c = 0, v_v)", [])),
19.66 - (Problem.prep_input thy "pbl_test_uni_root" [] Problem.id_empty
19.67 + (Problem.prep_input @{theory} "pbl_test_uni_root" [] Problem.id_empty
19.68 (["squareroot", "univariate", "equation", "test"],
19.69 [("#Given" ,["equality e_e", "solveFor v_v"]),
19.70 ("#Where" ,["precond_rootpbl v_v"]),
19.71 @@ -815,19 +815,19 @@
19.72 Rule_Set.append_rules "contains_root" Rule_Set.empty [Rule.Eval ("Test.contains_root",
19.73 eval_contains_root "#contains_root_")],
19.74 SOME "solve (e_e::bool, v_v)", [["Test", "square_equation"]])),
19.75 - (Problem.prep_input thy "pbl_test_uni_norm" [] Problem.id_empty
19.76 + (Problem.prep_input @{theory} "pbl_test_uni_norm" [] Problem.id_empty
19.77 (["normalise", "univariate", "equation", "test"],
19.78 [("#Given" ,["equality e_e", "solveFor v_v"]),
19.79 ("#Where" ,[]),
19.80 ("#Find" ,["solutions v_v'i'"])],
19.81 Rule_Set.empty, SOME "solve (e_e::bool, v_v)", [["Test", "norm_univar_equation"]])),
19.82 - (Problem.prep_input thy "pbl_test_uni_roottest" [] Problem.id_empty
19.83 + (Problem.prep_input @{theory} "pbl_test_uni_roottest" [] Problem.id_empty
19.84 (["sqroot-test", "univariate", "equation", "test"],
19.85 [("#Given" ,["equality e_e", "solveFor v_v"]),
19.86 ("#Where" ,["precond_rootpbl v_v"]),
19.87 ("#Find" ,["solutions v_v'i'"])],
19.88 Rule_Set.empty, SOME "solve (e_e::bool, v_v)", [])),
19.89 - (Problem.prep_input thy "pbl_test_intsimp" [] Problem.id_empty
19.90 + (Problem.prep_input @{theory} "pbl_test_intsimp" [] Problem.id_empty
19.91 (["inttype", "test"],
19.92 [("#Given" ,["intTestGiven t_t"]),
19.93 ("#Where" ,[]),
19.94 @@ -853,7 +853,7 @@
19.95 in
19.96 [e_e])"
19.97 setup \<open>KEStore_Elems.add_mets
19.98 - [MethodC.prep_input thy "met_test_solvelin" [] MethodC.id_empty
19.99 + [MethodC.prep_input @{theory} "met_test_solvelin" [] MethodC.id_empty
19.100 (["Test", "solve_linear"],
19.101 [("#Given" ,["equality e_e", "solveFor v_v"]),
19.102 ("#Where" ,["matches (?a = ?b) e_e"]),
19.103 @@ -884,7 +884,7 @@
19.104 in
19.105 [e_e])"
19.106 setup \<open>KEStore_Elems.add_mets
19.107 - [MethodC.prep_input thy "met_test_sqrt" [] MethodC.id_empty
19.108 + [MethodC.prep_input @{theory} "met_test_sqrt" [] MethodC.id_empty
19.109 (*root-equation, version for tests before 8.01.01*)
19.110 (["Test", "sqrt-equ-test"],
19.111 [("#Given" ,["equality e_e", "solveFor v_v"]),
19.112 @@ -912,7 +912,7 @@
19.113 in
19.114 Check_elementwise L_L {(v_v::real). Assumptions})"
19.115 setup \<open>KEStore_Elems.add_mets
19.116 - [MethodC.prep_input thy "met_test_squ_sub" [] MethodC.id_empty
19.117 + [MethodC.prep_input @{theory} "met_test_squ_sub" [] MethodC.id_empty
19.118 (*tests subproblem fixed linear*)
19.119 (["Test", "squ-equ-test-subpbl1"],
19.120 [("#Given" ,["equality e_e", "solveFor v_v"]),
19.121 @@ -944,7 +944,7 @@
19.122 in
19.123 Check_elementwise L_L {(v_v::real). Assumptions}) "
19.124 setup \<open>KEStore_Elems.add_mets
19.125 - [MethodC.prep_input thy "met_test_eq1" [] MethodC.id_empty
19.126 + [MethodC.prep_input @{theory} "met_test_eq1" [] MethodC.id_empty
19.127 (*root-equation1:*)
19.128 (["Test", "square_equation1"],
19.129 [("#Given" ,["equality e_e", "solveFor v_v"]),
19.130 @@ -977,7 +977,7 @@
19.131 in
19.132 Check_elementwise L_L {(v_v::real). Assumptions})"
19.133 setup \<open>KEStore_Elems.add_mets
19.134 - [MethodC.prep_input thy "met_test_squ2" [] MethodC.id_empty
19.135 + [MethodC.prep_input @{theory} "met_test_squ2" [] MethodC.id_empty
19.136 (*root-equation2*)
19.137 (["Test", "square_equation2"],
19.138 [("#Given" ,["equality e_e", "solveFor v_v"]),
19.139 @@ -1010,7 +1010,7 @@
19.140 in
19.141 Check_elementwise L_L {(v_v::real). Assumptions})"
19.142 setup \<open>KEStore_Elems.add_mets
19.143 - [MethodC.prep_input thy "met_test_squeq" [] MethodC.id_empty
19.144 + [MethodC.prep_input @{theory} "met_test_squeq" [] MethodC.id_empty
19.145 (*root-equation*)
19.146 (["Test", "square_equation"],
19.147 [("#Given" ,["equality e_e", "solveFor v_v"]),
19.148 @@ -1036,7 +1036,7 @@
19.149 in
19.150 Or_to_List e_e)"
19.151 setup \<open>KEStore_Elems.add_mets
19.152 - [MethodC.prep_input thy "met_test_eq_plain" [] MethodC.id_empty
19.153 + [MethodC.prep_input @{theory} "met_test_eq_plain" [] MethodC.id_empty
19.154 (*solve_plain_square*)
19.155 (["Test", "solve_plain_square"],
19.156 [("#Given",["equality e_e", "solveFor v_v"]),
20.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Thu Jun 10 11:54:20 2021 +0200
20.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Thu Jun 10 12:23:57 2021 +0200
20.3 @@ -885,8 +885,8 @@
20.4 \em Z\_Transform\normalfont.\<close>
20.5
20.6 setup \<open>KEStore_Elems.add_pbts
20.7 - [Problem.prep_input thy "pbl_SP" [] Problem.id_empty (["SignalProcessing"], [], Rule_Set.empty, NONE, []),
20.8 - Problem.prep_input thy "pbl_SP_Ztrans" [] Problem.id_empty
20.9 + [Problem.prep_input @{theory} "pbl_SP" [] Problem.id_empty (["SignalProcessing"], [], Rule_Set.empty, NONE, []),
20.10 + Problem.prep_input @{theory} "pbl_SP_Ztrans" [] Problem.id_empty
20.11 (["Z_Transform", "SignalProcessing"], [], Rule_Set.empty, NONE, [])]\<close>
20.12
20.13 text\<open>\noindent For the suddenly created node we have to define the input
20.14 @@ -894,7 +894,7 @@
20.15 Section~\ref{sec:deffdes}.\<close>
20.16
20.17 setup \<open>KEStore_Elems.add_pbts
20.18 - [Problem.prep_input thy "pbl_SP_Ztrans_inv" [] Problem.id_empty
20.19 + [Problem.prep_input @{theory} "pbl_SP_Ztrans_inv" [] Problem.id_empty
20.20 (["Inverse", "Z_Transform", "SignalProcessing"],
20.21 [("#Given" ,["filterExpression X_eq"]),
20.22 ("#Find", ["stepResponse n_eq"])],
20.23 @@ -923,12 +923,12 @@
20.24 as content.\<close>
20.25
20.26 setup \<open>KEStore_Elems.add_mets
20.27 - [MethodC.prep_input thy "met_SP" [] e_metID
20.28 + [MethodC.prep_input @{theory} "met_SP" [] e_metID
20.29 (["SignalProcessing"], [],
20.30 {rew_ord'="tless_true", rls'= Rule_Set.empty, calc = [], srls = Rule_Set.empty, prls = Rule_Set.empty, crls = Rule_Set.empty,
20.31 errpats = [], nrls = Rule_Set.empty},
20.32 "empty_script"),
20.33 - MethodC.prep_input thy "met_SP_Ztrans" [] e_metID
20.34 + MethodC.prep_input @{theory} "met_SP_Ztrans" [] e_metID
20.35 (["SignalProcessing", "Z_Transform"], [],
20.36 {rew_ord'="tless_true", rls'= Rule_Set.empty, calc = [], srls = Rule_Set.empty, prls = Rule_Set.empty, crls = Rule_Set.empty,
20.37 errpats = [], nrls = Rule_Set.empty},
21.1 --- a/test/Tools/isac/Specify/refine.thy Thu Jun 10 11:54:20 2021 +0200
21.2 +++ b/test/Tools/isac/Specify/refine.thy Thu Jun 10 12:23:57 2021 +0200
21.3 @@ -14,7 +14,7 @@
21.4
21.5 section \<open>data for test "-ptyps.thy: store test-pbtyps by 'setup' ---"\<close>
21.6 setup \<open>KEStore_Elems.add_pbts
21.7 -[(Problem.prep_input thy "pbl_test_refine" [] Problem.id_empty
21.8 +[(Problem.prep_input @{theory} "pbl_test_refine" [] Problem.id_empty
21.9 (["refine", "test"], [], Rule_Set.empty, NONE, [])),
21.10 (Problem.prep_input @{theory DiffApp} "pbl_pbla" [] Problem.id_empty
21.11 (["pbla", "refine", "test"],