1.1 --- a/src/Tools/isac/Knowledge/PolyMinus.thy Wed Dec 14 14:20:25 2016 +0100
1.2 +++ b/src/Tools/isac/Knowledge/PolyMinus.thy Sun Dec 18 16:27:41 2016 +0100
1.3 @@ -397,9 +397,9 @@
1.4
1.5 (** problems **)
1.6 setup {* KEStore_Elems.add_pbts
1.7 - [(prep_pbt thy "pbl_vereinf_poly" [] e_pblID
1.8 + [(Specify.prep_pbt thy "pbl_vereinf_poly" [] e_pblID
1.9 (["polynom","vereinfachen"], [], Erls, NONE, [])),
1.10 - (prep_pbt thy "pbl_vereinf_poly_minus" [] e_pblID
1.11 + (Specify.prep_pbt thy "pbl_vereinf_poly_minus" [] e_pblID
1.12 (["plus_minus","polynom","vereinfachen"],
1.13 [("#Given", ["Term t_t"]),
1.14 ("#Where", ["t_t is_polyexp",
1.15 @@ -424,7 +424,7 @@
1.16 Thm ("not_false",num_str @{thm not_false})
1.17 (*"(~ False) = True"*)],
1.18 SOME "Vereinfache t_t", [["simplification","for_polynomials","with_minus"]])),
1.19 - (prep_pbt thy "pbl_vereinf_poly_klammer" [] e_pblID
1.20 + (Specify.prep_pbt thy "pbl_vereinf_poly_klammer" [] e_pblID
1.21 (["klammer","polynom","vereinfachen"],
1.22 [("#Given" ,["Term t_t"]),
1.23 ("#Where" ,["t_t is_polyexp",
1.24 @@ -446,7 +446,7 @@
1.25 (*"(~ False) = True"*)],
1.26 SOME "Vereinfache t_t",
1.27 [["simplification","for_polynomials","with_parentheses"]])),
1.28 - (prep_pbt thy "pbl_vereinf_poly_klammer_mal" [] e_pblID
1.29 + (Specify.prep_pbt thy "pbl_vereinf_poly_klammer_mal" [] e_pblID
1.30 (["binom_klammer","polynom","vereinfachen"],
1.31 [("#Given", ["Term t_t"]),
1.32 ("#Where", ["t_t is_polyexp"]),
1.33 @@ -455,8 +455,8 @@
1.34 Calc ("Poly.is'_polyexp", eval_is_polyexp "")],
1.35 SOME "Vereinfache t_t",
1.36 [["simplification","for_polynomials","with_parentheses_mult"]])),
1.37 - (prep_pbt thy "pbl_probe" [] e_pblID (["probe"], [], Erls, NONE, [])),
1.38 - (prep_pbt thy "pbl_probe_poly" [] e_pblID
1.39 + (Specify.prep_pbt thy "pbl_probe" [] e_pblID (["probe"], [], Erls, NONE, [])),
1.40 + (Specify.prep_pbt thy "pbl_probe_poly" [] e_pblID
1.41 (["polynom","probe"],
1.42 [("#Given", ["Pruefe e_e", "mitWert w_w"]),
1.43 ("#Where", ["e_e is_polyexp"]),
1.44 @@ -465,7 +465,7 @@
1.45 Calc ("Poly.is'_polyexp", eval_is_polyexp "")],
1.46 SOME "Probe e_e w_w",
1.47 [["probe","fuer_polynom"]])),
1.48 - (prep_pbt thy "pbl_probe_bruch" [] e_pblID
1.49 + (Specify.prep_pbt thy "pbl_probe_bruch" [] e_pblID
1.50 (["bruch","probe"],
1.51 [("#Given" ,["Pruefe e_e", "mitWert w_w"]),
1.52 ("#Where" ,["e_e is_ratpolyexp"]),
1.53 @@ -476,7 +476,7 @@
1.54
1.55 (** methods **)
1.56 setup {* KEStore_Elems.add_mets
1.57 - [prep_met thy "met_simp_poly_minus" [] e_metID
1.58 + [Specify.prep_met thy "met_simp_poly_minus" [] e_metID
1.59 (["simplification","for_polynomials","with_minus"],
1.60 [("#Given" ,["Term t_t"]),
1.61 ("#Where" ,["t_t is_polyexp",
1.62 @@ -502,7 +502,7 @@
1.63 " ((Repeat((Try (Rewrite_Set ordne_alphabetisch False)) @@ " ^
1.64 " (Try (Rewrite_Set fasse_zusammen False)) @@ " ^
1.65 " (Try (Rewrite_Set verschoenere False)))) t_t)"),
1.66 - prep_met thy "met_simp_poly_parenth" [] e_metID
1.67 + Specify.prep_met thy "met_simp_poly_parenth" [] e_metID
1.68 (["simplification","for_polynomials","with_parentheses"],
1.69 [("#Given" ,["Term t_t"]),
1.70 ("#Where" ,["t_t is_polyexp"]),
1.71 @@ -516,7 +516,7 @@
1.72 " (Try (Rewrite_Set ordne_alphabetisch False)) @@ " ^
1.73 " (Try (Rewrite_Set fasse_zusammen False)) @@ " ^
1.74 " (Try (Rewrite_Set verschoenere False)))) t_t)"),
1.75 - prep_met thy "met_simp_poly_parenth_mult" [] e_metID
1.76 + Specify.prep_met thy "met_simp_poly_parenth_mult" [] e_metID
1.77 (["simplification","for_polynomials","with_parentheses_mult"],
1.78 [("#Given" ,["Term t_t"]), ("#Where" ,["t_t is_polyexp"]), ("#Find" ,["normalform n_n"])],
1.79 {rew_ord'="tless_true", rls' = e_rls, calc = [], srls = e_rls,
1.80 @@ -531,12 +531,12 @@
1.81 " (Try (Rewrite_Set ordne_alphabetisch False)) @@ " ^
1.82 " (Try (Rewrite_Set fasse_zusammen False)) @@ " ^
1.83 " (Try (Rewrite_Set verschoenere False)))) t_t)"),
1.84 - prep_met thy "met_probe" [] e_metID
1.85 + Specify.prep_met thy "met_probe" [] e_metID
1.86 (["probe"], [],
1.87 {rew_ord'="tless_true", rls' = e_rls, calc = [], srls = e_rls, prls = Erls, crls = e_rls,
1.88 errpats = [], nrls = Erls},
1.89 "empty_script"),
1.90 - prep_met thy "met_probe_poly" [] e_metID
1.91 + Specify.prep_met thy "met_probe_poly" [] e_metID
1.92 (["probe","fuer_polynom"],
1.93 [("#Given" ,["Pruefe e_e", "mitWert w_w"]),
1.94 ("#Where" ,["e_e is_polyexp"]),
1.95 @@ -551,7 +551,7 @@
1.96 " in (Repeat((Try (Repeat (Calculate TIMES))) @@ " ^
1.97 " (Try (Repeat (Calculate PLUS ))) @@ " ^
1.98 " (Try (Repeat (Calculate MINUS))))) e_e)"),
1.99 - prep_met thy "met_probe_bruch" [] e_metID
1.100 + Specify.prep_met thy "met_probe_bruch" [] e_metID
1.101 (["probe","fuer_bruch"],
1.102 [("#Given" ,["Pruefe e_e", "mitWert w_w"]),
1.103 ("#Where" ,["e_e is_ratpolyexp"]),