1.1 --- a/src/Tools/isac/Knowledge/AlgEin.thy	Wed Nov 21 12:32:54 2018 +0100
     1.2 +++ b/src/Tools/isac/Knowledge/AlgEin.thy	Wed Nov 28 11:46:00 2018 +0100
     1.3 @@ -36,17 +36,19 @@
     1.4          Rule.e_rls, NONE, [["Berechnung","erstNumerisch"], ["Berechnung","erstSymbolisch"]]))];\<close>
     1.5  
     1.6  setup \<open>KEStore_Elems.add_mets
     1.7 -  [Specify.prep_met thy "met_algein" [] Celem.e_metID
     1.8 +    [Specify.prep_met thy "met_algein" [] Celem.e_metID
     1.9  	    (["Berechnung"], [],
    1.10  	      {rew_ord'="tless_true", rls'= Rule.Erls, calc = [], srls = Rule.Erls, prls = Rule.Erls, crls =Rule.Erls,
    1.11            errpats = [], nrls = Rule.Erls},
    1.12 -        "empty_script"),
    1.13 +          "empty_script"),
    1.14      Specify.prep_met thy "met_algein_numsym" [] Celem.e_metID
    1.15  	    (["Berechnung","erstNumerisch"], [],
    1.16  	      {rew_ord'="tless_true", rls'= Rule.Erls, calc = [], srls = Rule.Erls, prls = Rule.Erls, crls =Rule.Erls,
    1.17  	        errpats = [], nrls = Rule.Erls},
    1.18 -	      "empty_script"),
    1.19 -    Specify.prep_met thy "met_algein_numsym" [] Celem.e_metID
    1.20 +	      "empty_script")]
    1.21 +\<close>
    1.22 +setup \<open>KEStore_Elems.add_mets
    1.23 +    [Specify.prep_met thy "met_algein_numsym_1num" [] Celem.e_metID
    1.24  	    (["Berechnung","erstNumerisch"],
    1.25  	       [("#Given" ,["KantenLaenge k_k","Querschnitt q__q", "KantenUnten u_u",
    1.26  	           "KantenSenkrecht s_s", "KantenOben o_o"]),
    1.27 @@ -73,8 +75,10 @@
    1.28             "      t_t = Substitute u_u t_t;                                " ^
    1.29             "      t_t = Substitute [k_k, q__q] t_t;                         " ^
    1.30             "      t_t = (Repeat (Try (Rewrite_Set norm_Poly False))) t_t  " ^
    1.31 -           " in (Try (Rewrite_Set norm_Poly False)) t_t)                  "),
    1.32 -    Specify.prep_met thy "met_algein_symnum" [] Celem.e_metID
    1.33 +           " in (Try (Rewrite_Set norm_Poly False)) t_t)                  ")]
    1.34 +\<close>
    1.35 +setup \<open>KEStore_Elems.add_mets
    1.36 +    [Specify.prep_met thy "met_algein_symnum" [] Celem.e_metID
    1.37  	    (["Berechnung","erstSymbolisch"],
    1.38  	        [("#Given" ,["KantenLaenge k_k","Querschnitt q__q", "KantenUnten u_u",
    1.39                  "KantenSenkrecht s_s", "KantenOben o_o"]),

     2.1 --- a/src/Tools/isac/Knowledge/Biegelinie.thy	Wed Nov 21 12:32:54 2018 +0100
     2.2 +++ b/src/Tools/isac/Knowledge/Biegelinie.thy	Wed Nov 28 11:46:00 2018 +0100
     2.3 @@ -189,7 +189,7 @@
     2.4  subsection \<open>Sub-problem "integrate and determine constants", little modularisation\<close>
     2.5  
     2.6  setup \<open>KEStore_Elems.add_mets
     2.7 -  [Specify.prep_met @{theory} "met_biege" [] Celem.e_metID 
     2.8 +    [Specify.prep_met @{theory} "met_biege" [] Celem.e_metID 
     2.9  	    (["IntegrierenUndKonstanteBestimmen"],
    2.10  	      [("#Given" ,["Traegerlaenge l_l", "Streckenlast q__q", "FunktionsVariable v_v"]),
    2.11  		      (*("#Where",["0 < l_l"]), ...wait for &lt; and handling Arbfix*)
    2.12 @@ -297,7 +297,7 @@
    2.13   \\\------------------------------------------------------------------------------------*)
    2.14  
    2.15  setup \<open>KEStore_Elems.add_mets
    2.16 -  [Specify.prep_met @{theory} "met_biege_2" [] Celem.e_metID
    2.17 +    [Specify.prep_met @{theory} "met_biege_2" [] Celem.e_metID
    2.18  	    (["IntegrierenUndKonstanteBestimmen2"],
    2.19  	      [("#Given" ,["Traegerlaenge l", "Streckenlast q", "FunktionsVariable v"]),
    2.20  		      (*("#Where",["0 < l"]), ...wait for &lt; and handling Arbfix*)
    2.21 @@ -331,8 +331,10 @@
    2.22          "    B = Take (lastI funs);                                                         " ^
    2.23          "    B = ((Substitute cons) @@                                                      " ^
    2.24          "           (Rewrite_Set_Inst [(bdv, v)] make_ratpoly_in False)) B                  " ^
    2.25 -        "  in B)                                                                           "),
    2.26 -    Specify.prep_met @{theory} "met_biege_intconst_2" [] Celem.e_metID
    2.27 +        "  in B)                                                                           ")]
    2.28 +\<close>
    2.29 +setup \<open>KEStore_Elems.add_mets
    2.30 +    [Specify.prep_met @{theory} "met_biege_intconst_2" [] Celem.e_metID
    2.31  	    (["IntegrierenUndKonstanteBestimmen","2xIntegrieren"], [],
    2.32  	      {rew_ord'="tless_true", rls'=Rule.Erls, calc = [], srls = Rule.e_rls, prls=Rule.e_rls, crls = Atools_erls,
    2.33            errpats = [], nrls = Rule.e_rls},
    2.34 @@ -356,7 +358,7 @@
    2.35  subsection \<open>Compute the general bending line\<close>
    2.36  
    2.37  setup \<open>KEStore_Elems.add_mets
    2.38 -  [Specify.prep_met @{theory} "met_biege_ausbelast" [] Celem.e_metID
    2.39 +    [Specify.prep_met @{theory} "met_biege_ausbelast" [] Celem.e_metID
    2.40  	    (["Biegelinien", "ausBelastung"],
    2.41  	      [("#Given" ,["Streckenlast q__q", "FunktionsVariable v_v"]),
    2.42  	        ("#Find"  ,["Funktionen fun_s"])],
    2.43 @@ -397,7 +399,7 @@
    2.44  subsection \<open>Substitute the constraints into the equations\<close>
    2.45  
    2.46  setup \<open>KEStore_Elems.add_mets
    2.47 -  [Specify.prep_met @{theory} "met_biege_setzrand" [] Celem.e_metID
    2.48 +    [Specify.prep_met @{theory} "met_biege_setzrand" [] Celem.e_metID
    2.49  	    (["Biegelinien", "setzeRandbedingungenEin"],
    2.50  	      [("#Given" , ["Funktionen fun_s", "Randbedingungen r_b"]),
    2.51  	        ("#Find"  , ["Gleichungen equs'''"])],
    2.52 @@ -460,7 +462,7 @@
    2.53  subsection \<open>Transform an equality into a function\<close>
    2.54  
    2.55  setup \<open>KEStore_Elems.add_mets
    2.56 -  [Specify.prep_met @{theory} "met_equ_fromfun" [] Celem.e_metID
    2.57 +    [Specify.prep_met @{theory} "met_equ_fromfun" [] Celem.e_metID
    2.58  	    (["Equation","fromFunction"],
    2.59  	      [("#Given" ,["functionEq fu_n","substitution su_b"]),
    2.60  	        ("#Find"  ,["equality equ'''"])],

     3.1 --- a/src/Tools/isac/Knowledge/Diff.thy	Wed Nov 21 12:32:54 2018 +0100
     3.2 +++ b/src/Tools/isac/Knowledge/Diff.thy	Wed Nov 28 11:46:00 2018 +0100
     3.3 @@ -281,12 +281,14 @@
     3.4    | argl2dtss _ = error "Diff.ML: wrong argument for argl2dtss";
     3.5  \<close>
     3.6  setup \<open>KEStore_Elems.add_mets
     3.7 -  [Specify.prep_met thy "met_diff" [] Celem.e_metID
     3.8 +    [Specify.prep_met thy "met_diff" [] Celem.e_metID
     3.9        (["diff"], [],
    3.10          {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = Rule.e_rls, prls=Rule.e_rls,
    3.11            crls = Atools_erls, errpats = [], nrls = norm_diff},
    3.12 -        "empty_script"),
    3.13 -    Specify.prep_met thy "met_diff_onR" [] Celem.e_metID
    3.14 +        "empty_script")]
    3.15 +\<close>
    3.16 +setup \<open>KEStore_Elems.add_mets
    3.17 +    [Specify.prep_met thy "met_diff_onR" [] Celem.e_metID
    3.18        (["diff","differentiate_on_R"],
    3.19          [("#Given" ,["functionTerm f_f","differentiateFor v_v"]),
    3.20            ("#Find"  ,["derivative f_f'"])],
    3.21 @@ -313,8 +315,10 @@
    3.22            "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_const      False)) Or " ^
    3.23            "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_var        False)) Or " ^
    3.24            "    (Repeat (Rewrite_Set             make_polynomial False)))) @@ " ^
    3.25 -          " (Try (Rewrite_Set_Inst [(bdv,v_v)] diff_sym_conv False)))) f_f')"),
    3.26 -    Specify.prep_met thy "met_diff_simpl" [] Celem.e_metID
    3.27 +          " (Try (Rewrite_Set_Inst [(bdv,v_v)] diff_sym_conv False)))) f_f')")]
    3.28 +\<close>
    3.29 +setup \<open>KEStore_Elems.add_mets
    3.30 +    [Specify.prep_met thy "met_diff_simpl" [] Celem.e_metID
    3.31        (["diff","diff_simpl"],
    3.32          [("#Given", ["functionTerm f_f","differentiateFor v_v"]),
    3.33           ("#Find" , ["derivative f_f'"])],
    3.34 @@ -341,8 +345,10 @@
    3.35            "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_const      False)) Or " ^
    3.36            "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_var        False)) Or " ^
    3.37            "    (Repeat (Rewrite_Set              make_polynomial False))))  " ^
    3.38 -          " )) f_f')"),
    3.39 -    Specify.prep_met thy "met_diff_equ" [] Celem.e_metID
    3.40 +          " )) f_f')")]
    3.41 +\<close>
    3.42 +setup \<open>KEStore_Elems.add_mets
    3.43 +    [Specify.prep_met thy "met_diff_equ" [] Celem.e_metID
    3.44        (["diff","differentiate_equality"],
    3.45          [("#Given" ,["functionEq f_f","differentiateFor v_v"]),
    3.46            ("#Find"  ,["derivativeEq f_f'"])],
    3.47 @@ -370,8 +376,10 @@
    3.48            "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_const      False)) Or   " ^
    3.49            "    (Repeat (Rewrite_Inst [(bdv,v_v)] diff_var        False)) Or   " ^
    3.50            "    (Repeat (Rewrite_Set             make_polynomial False)))) @@ " ^
    3.51 -          " (Try (Rewrite_Set_Inst [(bdv,v_v)] diff_sym_conv False)))) f_f')"),
    3.52 -    Specify.prep_met thy "met_diff_after_simp" [] Celem.e_metID
    3.53 +          " (Try (Rewrite_Set_Inst [(bdv,v_v)] diff_sym_conv False)))) f_f')")]
    3.54 +\<close>
    3.55 +setup \<open>KEStore_Elems.add_mets
    3.56 +    [Specify.prep_met thy "met_diff_after_simp" [] Celem.e_metID
    3.57        (["diff","after_simplification"],
    3.58          [("#Given" ,["functionTerm f_f","differentiateFor v_v"]),
    3.59            ("#Find"  ,["derivative f_f'"])],

     4.1 --- a/src/Tools/isac/Knowledge/DiffApp.thy	Wed Nov 21 12:32:54 2018 +0100
     4.2 +++ b/src/Tools/isac/Knowledge/DiffApp.thy	Wed Nov 28 11:46:00 2018 +0100
     4.3 @@ -117,12 +117,14 @@
     4.4  
     4.5  (** methods, scripts not yet implemented **)
     4.6  setup \<open>KEStore_Elems.add_mets
     4.7 -  [Specify.prep_met thy "met_diffapp" [] Celem.e_metID
     4.8 +    [Specify.prep_met thy "met_diffapp" [] Celem.e_metID
     4.9        (["DiffApp"], [],
    4.10          {rew_ord'="tless_true", rls'=Atools_erls,calc = [], srls = Rule.e_rls, prls = Rule.e_rls,
    4.11            crls = Atools_erls, errpats = [], nrls = norm_Rational (*, asm_rls=[],asm_thm=[]*)},
    4.12 -        "empty_script"),
    4.13 -    Specify.prep_met thy "met_diffapp_max" [] Celem.e_metID
    4.14 +        "empty_script")]
    4.15 +\<close>
    4.16 +setup \<open>KEStore_Elems.add_mets
    4.17 +    [Specify.prep_met thy "met_diffapp_max" [] Celem.e_metID
    4.18        (["DiffApp","max_by_calculus"],
    4.19          [("#Given" ,["fixedValues f_ix","maximum m_m","relations r_s", "boundVariable v_v",
    4.20                "interval i_tv","errorBound e_rr"]),
    4.21 @@ -143,8 +145,10 @@
    4.22            "                               [BOOL t_t, REAL v_v, REAL_SET i_tv]    " ^
    4.23            " in ((SubProblem (DiffApp',[find_values,tool],[Isac,find_values])      " ^
    4.24            "      [REAL m_x, REAL (Rhs t_t), REAL v_v, REAL m_m,                  " ^
    4.25 -          "       BOOL_LIST (dropWhile (ident e_e) r_s)])::bool list))            "),
    4.26 -    Specify.prep_met thy "met_diffapp_funnew" [] Celem.e_metID
    4.27 +          "       BOOL_LIST (dropWhile (ident e_e) r_s)])::bool list))            ")]
    4.28 +\<close>
    4.29 +setup \<open>KEStore_Elems.add_mets
    4.30 +    [Specify.prep_met thy "met_diffapp_funnew" [] Celem.e_metID
    4.31        (["DiffApp","make_fun_by_new_variable"],
    4.32          [("#Given" ,["functionOf f_f","boundVariable v_v","equalities eqs"]),
    4.33            ("#Find"  ,["functionEq f_1"])],
    4.34 @@ -165,8 +169,10 @@
    4.35            "  (s_2::bool list) =                                                 " ^
    4.36            "                (SubProblem (DiffApp',[univariate,equation],[no_met])" ^
    4.37            "                    [BOOL e_2, REAL v_2])" ^
    4.38 -          "in Substitute [(v_1 = (rhs o hd) s_1),(v_2 = (rhs o hd) s_2)] h_h)"),
    4.39 -    Specify.prep_met thy "met_diffapp_funexp" [] Celem.e_metID
    4.40 +          "in Substitute [(v_1 = (rhs o hd) s_1),(v_2 = (rhs o hd) s_2)] h_h)")]
    4.41 +\<close>
    4.42 +setup \<open>KEStore_Elems.add_mets
    4.43 +    [Specify.prep_met thy "met_diffapp_funexp" [] Celem.e_metID
    4.44        (["DiffApp","make_fun_by_explicit"],
    4.45          [("#Given" ,["functionOf f_f","boundVariable v_v","equalities eqs"]),
    4.46            ("#Find"  ,["functionEq f_1"])],
    4.47 @@ -181,8 +187,10 @@
    4.48            "      (s_1::bool list)=                                           " ^ 
    4.49            "              (SubProblem(DiffApp',[univariate,equation],[no_met])" ^
    4.50            "                          [BOOL e_1, REAL v_1])                 " ^
    4.51 -          " in Substitute [(v_1 = (rhs o hd) s_1)] h_h)                       "),
    4.52 -    Specify.prep_met thy "met_diffapp_max_oninterval" [] Celem.e_metID
    4.53 +          " in Substitute [(v_1 = (rhs o hd) s_1)] h_h)                       ")]
    4.54 +\<close>
    4.55 +setup \<open>KEStore_Elems.add_mets
    4.56 +    [Specify.prep_met thy "met_diffapp_max_oninterval" [] Celem.e_metID
    4.57        (["DiffApp","max_on_interval_by_calculus"],
    4.58          [("#Given" ,["functionEq t_t","boundVariable v_v","interval i_tv"(*, "errorBound e_rr"*)]),
    4.59            ("#Find"  ,["maxArgument v_0"])],

     5.1 --- a/src/Tools/isac/Knowledge/DiophantEq.thy	Wed Nov 21 12:32:54 2018 +0100
     5.2 +++ b/src/Tools/isac/Knowledge/DiophantEq.thy	Wed Nov 28 11:46:00 2018 +0100
     5.3 @@ -30,7 +30,7 @@
     5.4  
     5.5  text \<open>method solving the usecase\<close>
     5.6  setup \<open>KEStore_Elems.add_mets
     5.7 -  [Specify.prep_met thy "met_test_diophant" [] Celem.e_metID
     5.8 +    [Specify.prep_met thy "met_test_diophant" [] Celem.e_metID
     5.9        (["Test","solve_diophant"],
    5.10          [("#Given" ,["boolTestGiven e_e","intTestGiven (v_v::int)"]),
    5.11            (*                                      TODO: drop ^^^^^*)

     6.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy	Wed Nov 21 12:32:54 2018 +0100
     6.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy	Wed Nov 28 11:46:00 2018 +0100
     6.3 @@ -516,7 +516,7 @@
     6.4  
     6.5  (**methods**)
     6.6  setup \<open>KEStore_Elems.add_mets
     6.7 -  [Specify.prep_met thy "met_eqsys" [] Celem.e_metID
     6.8 +    [Specify.prep_met thy "met_eqsys" [] Celem.e_metID
     6.9  	    (["EqSystem"], [],
    6.10  	      {rew_ord'="tless_true", rls' = Rule.Erls, calc = [], srls = Rule.Erls, prls = Rule.Erls, crls = Rule.Erls,
    6.11            errpats = [], nrls = Rule.Erls},
    6.12 @@ -525,8 +525,10 @@
    6.13        (["EqSystem","top_down_substitution"], [],
    6.14          {rew_ord'="tless_true", rls' = Rule.Erls, calc = [], srls = Rule.Erls, prls = Rule.Erls, crls = Rule.Erls,
    6.15            errpats = [], nrls = Rule.Erls},
    6.16 -       "empty_script"),
    6.17 -    Specify.prep_met thy "met_eqsys_topdown_2x2" [] Celem.e_metID
    6.18 +       "empty_script")]
    6.19 +\<close>
    6.20 +setup \<open>KEStore_Elems.add_mets
    6.21 +    [Specify.prep_met thy "met_eqsys_topdown_2x2" [] Celem.e_metID
    6.22        (["EqSystem", "top_down_substitution", "2x2"],
    6.23          [("#Given", ["equalities e_s", "solveForVars v_s"]),
    6.24            ("#Where",
    6.25 @@ -571,13 +573,17 @@
    6.26            "                              isolate_bdvs False))              @@   " ^
    6.27            "       (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^
    6.28            "                                  simplify_System False))) e__s)"
    6.29 -          ---------------------------------------------------------------------------*)),
    6.30 -    Specify.prep_met thy "met_eqsys_norm" [] Celem.e_metID
    6.31 +          ---------------------------------------------------------------------------*))]
    6.32 +\<close>
    6.33 +setup \<open>KEStore_Elems.add_mets
    6.34 +    [Specify.prep_met thy "met_eqsys_norm" [] Celem.e_metID
    6.35  	    (["EqSystem", "normalise"], [],
    6.36  	      {rew_ord'="tless_true", rls' = Rule.Erls, calc = [], srls = Rule.Erls, prls = Rule.Erls, crls = Rule.Erls,
    6.37            errpats = [], nrls = Rule.Erls},
    6.38 -	      "empty_script"),
    6.39 -    Specify.prep_met thy "met_eqsys_norm_2x2" [] Celem.e_metID
    6.40 +	      "empty_script")]
    6.41 +\<close>
    6.42 +setup \<open>KEStore_Elems.add_mets
    6.43 +    [Specify.prep_met thy "met_eqsys_norm_2x2" [] Celem.e_metID
    6.44  	    (["EqSystem","normalise","2x2"],
    6.45  	      [("#Given" ,["equalities e_s", "solveForVars v_s"]),
    6.46  		      ("#Find"  ,["solution ss'''"])],
    6.47 @@ -597,8 +603,10 @@
    6.48            "                                  simplify_System_parenthesized False)) @@  " ^
    6.49            "               (Try (Rewrite_Set order_system False))) e_s                  " ^
    6.50            "   in (SubProblem (EqSystem',[LINEAR,system],[no_met])                      " ^
    6.51 -          "                  [BOOL_LIST e__s, REAL_LIST v_s]))"),
    6.52 -    Specify.prep_met thy "met_eqsys_norm_4x4" [] Celem.e_metID
    6.53 +          "                  [BOOL_LIST e__s, REAL_LIST v_s]))")]
    6.54 +\<close>
    6.55 +setup \<open>KEStore_Elems.add_mets
    6.56 +    [Specify.prep_met thy "met_eqsys_norm_4x4" [] Celem.e_metID
    6.57  	      (["EqSystem","normalise","4x4"],
    6.58  	       [("#Given" ,["equalities e_s", "solveForVars v_s"]),
    6.59  	         ("#Find"  ,["solution ss'''"])],
    6.60 @@ -624,8 +632,10 @@
    6.61             "                             simplify_System_parenthesized False))    @@    " ^
    6.62             "      (Try (Rewrite_Set order_system False)))                           e_s " ^
    6.63             "   in (SubProblem (EqSystem',[LINEAR,system],[no_met])                      " ^
    6.64 -           "                  [BOOL_LIST e__s, REAL_LIST v_s]))"),
    6.65 -    Specify.prep_met thy "met_eqsys_topdown_4x4" [] Celem.e_metID
    6.66 +           "                  [BOOL_LIST e__s, REAL_LIST v_s]))")]
    6.67 +\<close>
    6.68 +setup \<open>KEStore_Elems.add_mets
    6.69 +    [Specify.prep_met thy "met_eqsys_topdown_4x4" [] Celem.e_metID
    6.70  	    (["EqSystem","top_down_substitution","4x4"],
    6.71  	      [("#Given" ,["equalities e_s", "solveForVars v_s"]),
    6.72  	        ("#Where" , (*accepts missing variables up to diagonal form*)

     7.1 --- a/src/Tools/isac/Knowledge/Equation.thy	Wed Nov 21 12:32:54 2018 +0100
     7.2 +++ b/src/Tools/isac/Knowledge/Equation.thy	Wed Nov 28 11:46:00 2018 +0100
     7.3 @@ -86,7 +86,7 @@
     7.4  
     7.5  
     7.6  setup \<open>KEStore_Elems.add_mets
     7.7 -  [Specify.prep_met thy "met_equ" [] Celem.e_metID
     7.8 +    [Specify.prep_met thy "met_equ" [] Celem.e_metID
     7.9  	    (["Equation"], [],
    7.10  	      {rew_ord'="tless_true", rls'=Rule.Erls, calc = [], srls = Rule.e_rls, prls=Rule.e_rls, crls = Atools_erls,
    7.11            errpats = [], nrls = Rule.e_rls},

     8.1 --- a/src/Tools/isac/Knowledge/InsSort.thy	Wed Nov 21 12:32:54 2018 +0100
     8.2 +++ b/src/Tools/isac/Knowledge/InsSort.thy	Wed Nov 28 11:46:00 2018 +0100
     8.3 @@ -101,8 +101,10 @@
     8.4        (["Programming","SORT"], [],
     8.5          {rew_ord'="tless_true",rls' = Rule.e_rls, calc = [], srls = Rule.e_rls, prls = Rule.e_rls,
     8.6            crls = Rule.e_rls, errpats = [], nrls = Rule.e_rls},
     8.7 -        "empty_script"),
     8.8 -    Specify.prep_met @{theory} "met_Prog_sort_ins" [] Celem.e_metID
     8.9 +        "empty_script")]
    8.10 +\<close>
    8.11 +setup \<open>KEStore_Elems.add_mets
    8.12 +   [Specify.prep_met @{theory} "met_Prog_sort_ins" [] Celem.e_metID
    8.13        (["Programming","SORT","insertion"], 
    8.14        [("#Given", ["unsorted u_u"]), ("#Find", ["sorted s_s"])],
    8.15          {rew_ord'="tless_true",rls' = Atools_erls, calc = [], srls = Rule.e_rls, prls = Rule.e_rls,
    8.16 @@ -111,8 +113,10 @@
    8.17          "  (let uns = Take (sort unso) " ^
    8.18          "  in " ^
    8.19          "    (Rewrite_Set ins_sort False) uns" ^
    8.20 -        "  )"),
    8.21 -    Specify.prep_met @{theory} "met_Prog_sort_ins_steps" [] Celem.e_metID
    8.22 +        "  )")]
    8.23 +\<close>
    8.24 +setup \<open>KEStore_Elems.add_mets
    8.25 +   [Specify.prep_met @{theory} "met_Prog_sort_ins_steps" [] Celem.e_metID
    8.26        (["Programming","SORT","insertion_steps"], 
    8.27        [("#Given", ["unsorted u_u"]), ("#Find", ["sorted s_s"])],
    8.28          {rew_ord'="tless_true",rls' = Atools_erls, calc = [], srls = Rule.e_rls, prls = Rule.e_rls,

     9.1 --- a/src/Tools/isac/Knowledge/Integrate.thy	Wed Nov 21 12:32:54 2018 +0100
     9.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy	Wed Nov 28 11:46:00 2018 +0100
     9.3 @@ -356,15 +356,17 @@
     9.4  
     9.5  (** methods **)
     9.6  setup \<open>KEStore_Elems.add_mets
     9.7 -  [Specify.prep_met thy "met_diffint" [] Celem.e_metID
     9.8 +    [Specify.prep_met thy "met_diffint" [] Celem.e_metID
     9.9  	    (["diff","integration"],
    9.10  	      [("#Given" ,["functionTerm f_f", "integrateBy v_v"]), ("#Find"  ,["antiDerivative F_F"])],
    9.11  	      {rew_ord'="tless_true", rls'=Atools_erls, calc = [], srls = Rule.e_rls, prls=Rule.e_rls,
    9.12  	        crls = Atools_erls, errpats = [], nrls = Rule.e_rls},
    9.13  	      "Script IntegrationScript (f_f::real) (v_v::real) =                " ^
    9.14            "  (let t_t = Take (Integral f_f D v_v)                             " ^
    9.15 -          "   in (Rewrite_Set_Inst [(bdv,v_v)] integration False) (t_t::real))"),
    9.16 -    Specify.prep_met thy "met_diffint_named" [] Celem.e_metID
    9.17 +          "   in (Rewrite_Set_Inst [(bdv,v_v)] integration False) (t_t::real))")]
    9.18 +\<close>
    9.19 +setup \<open>KEStore_Elems.add_mets
    9.20 +    [Specify.prep_met thy "met_diffint_named" [] Celem.e_metID
    9.21  	    (["diff","integration","named"],
    9.22  	      [("#Given" ,["functionTerm f_f", "integrateBy v_v"]),
    9.23  	        ("#Find"  ,["antiDerivativeName F_F"])],

    10.1 --- a/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy	Wed Nov 21 12:32:54 2018 +0100
    10.2 +++ b/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy	Wed Nov 28 11:46:00 2018 +0100
    10.3 @@ -73,15 +73,17 @@
    10.4  subsection \<open>Setup Parent Nodes in Hierarchy of Method\<close>
    10.5  ML \<open>val thy = @{theory}; (*latest version of thy required*)\<close>
    10.6  setup \<open>KEStore_Elems.add_mets
    10.7 -  [Specify.prep_met thy "met_SP" [] Celem.e_metID
    10.8 +    [Specify.prep_met thy "met_SP" [] Celem.e_metID
    10.9        (["SignalProcessing"], [],
   10.10          {rew_ord'="tless_true", rls'= Rule.e_rls, calc = [], srls = Rule.e_rls, prls = Rule.e_rls, crls = Rule.e_rls,
   10.11            errpats = [], nrls = Rule.e_rls}, "empty_script"),
   10.12      Specify.prep_met thy "met_SP_Ztrans" [] Celem.e_metID
   10.13        (["SignalProcessing", "Z_Transform"], [],
   10.14          {rew_ord'="tless_true", rls'= Rule.e_rls, calc = [], srls = Rule.e_rls, prls = Rule.e_rls, crls = Rule.e_rls,
   10.15 -          errpats = [], nrls = Rule.e_rls}, "empty_script"),
   10.16 -    Specify.prep_met thy "met_SP_Ztrans_inv" [] Celem.e_metID
   10.17 +          errpats = [], nrls = Rule.e_rls}, "empty_script")]
   10.18 +\<close>
   10.19 +setup \<open>KEStore_Elems.add_mets
   10.20 +    [Specify.prep_met thy "met_SP_Ztrans_inv" [] Celem.e_metID
   10.21        (["SignalProcessing", "Z_Transform", "Inverse"], 
   10.22          [("#Given" ,["filterExpression (X_eq::bool)"]),
   10.23            ("#Find"  ,["stepResponse (n_eq::bool)"])],
   10.24 @@ -101,8 +103,10 @@
   10.25            "                         [LINEAR,univariate,equation,test]," ^
   10.26            "                         [Test,solve_linear])              " ^
   10.27            "                        [BOOL equ, REAL z])              " ^
   10.28 -          "  in X)"),
   10.29 -    Specify.prep_met thy "met_SP_Ztrans_inv" [] Celem.e_metID
   10.30 +          "  in X)")]
   10.31 +\<close>
   10.32 +setup \<open>KEStore_Elems.add_mets
   10.33 +    [Specify.prep_met thy "met_SP_Ztrans_inv" [] Celem.e_metID
   10.34        (["SignalProcessing", "Z_Transform", "Inverse"], 
   10.35          [("#Given" ,["filterExpression X_eq"]),
   10.36            ("#Find"  ,["stepResponse n_eq"])],
   10.37 @@ -174,8 +178,10 @@
   10.38             "      (X_z::bool) = Take (X_z = pbz);                          "^
   10.39             "      (n_eq::bool) = (Rewrite_Set inverse_z False) X_z;        "^
   10.40             "      n_eq = drop_questionmarks n_eq                           "^
   10.41 -           "in n_eq)"),
   10.42 -    Specify.prep_met thy "met_SP_Ztrans_inv_sub" [] Celem.e_metID
   10.43 +           "in n_eq)")]
   10.44 +\<close>
   10.45 +setup \<open>KEStore_Elems.add_mets
   10.46 +    [Specify.prep_met thy "met_SP_Ztrans_inv_sub" [] Celem.e_metID
   10.47        (["SignalProcessing", "Z_Transform", "Inverse_sub"], 
   10.48          [("#Given" ,["filterExpression X_eq"]),
   10.49            ("#Find"  ,["stepResponse n_eq"])],

    11.1 --- a/src/Tools/isac/Knowledge/LinEq.thy	Wed Nov 21 12:32:54 2018 +0100
    11.2 +++ b/src/Tools/isac/Knowledge/LinEq.thy	Wed Nov 28 11:46:00 2018 +0100
    11.3 @@ -133,13 +133,15 @@
    11.4  
    11.5  (*-------------- methods------------------------------------------------------*)
    11.6  setup \<open>KEStore_Elems.add_mets
    11.7 -  [Specify.prep_met thy "met_eqlin" [] Celem.e_metID
    11.8 +    [Specify.prep_met thy "met_eqlin" [] Celem.e_metID
    11.9        (["LinEq"], [],
   11.10          {rew_ord' = "tless_true",rls' = Atools_erls,calc = [], srls = Rule.e_rls, prls = Rule.e_rls,
   11.11            crls = LinEq_crls, errpats = [], nrls = norm_Poly},
   11.12 -        "empty_script"),
   11.13 +        "empty_script")]
   11.14 +\<close>
   11.15      (* ansprechen mit ["LinEq","solve_univar_equation"] *)
   11.16 -    Specify.prep_met thy "met_eq_lin" [] Celem.e_metID
   11.17 +setup \<open>KEStore_Elems.add_mets
   11.18 +    [Specify.prep_met thy "met_eq_lin" [] Celem.e_metID
   11.19        (["LinEq","solve_lineq_equation"],
   11.20          [("#Given", ["equality e_e", "solveFor v_v"]),
   11.21            ("#Where", ["Not ((lhs e_e) is_polyrat_in v_v)", "((lhs e_e)  has_degree_in v_v) = 1"]),

    12.1 --- a/src/Tools/isac/Knowledge/LogExp.thy	Wed Nov 21 12:32:54 2018 +0100
    12.2 +++ b/src/Tools/isac/Knowledge/LogExp.thy	Wed Nov 28 11:46:00 2018 +0100
    12.3 @@ -40,7 +40,7 @@
    12.4  
    12.5  (** methods **)
    12.6  setup \<open>KEStore_Elems.add_mets
    12.7 -  [Specify.prep_met thy "met_equ_log" [] Celem.e_metID
    12.8 +    [Specify.prep_met thy "met_equ_log" [] Celem.e_metID
    12.9        (["Equation","solve_log"],
   12.10          [("#Given" ,["equality e_e","solveFor v_v"]),
   12.11            ("#Where" ,["matches ((?a log ?v_v) = ?b) e_e"]),

    13.1 --- a/src/Tools/isac/Knowledge/Partial_Fractions.thy	Wed Nov 21 12:32:54 2018 +0100
    13.2 +++ b/src/Tools/isac/Knowledge/Partial_Fractions.thy	Wed Nov 28 11:46:00 2018 +0100
    13.3 @@ -223,7 +223,7 @@
    13.4  
    13.5  (* current version, error outcommented *)
    13.6  setup \<open>KEStore_Elems.add_mets
    13.7 -  [Specify.prep_met @{theory} "met_partial_fraction" [] Celem.e_metID
    13.8 +    [Specify.prep_met @{theory} "met_partial_fraction" [] Celem.e_metID
    13.9        (["simplification","of_rationals","to_partial_fraction"], 
   13.10          [("#Given" ,["functionTerm t_t", "solveFor v_v"]),
   13.11            (*("#Where" ,["((get_numerator t_t) has_degree_in v_v) < 

    14.1 --- a/src/Tools/isac/Knowledge/Poly.thy	Wed Nov 21 12:32:54 2018 +0100
    14.2 +++ b/src/Tools/isac/Knowledge/Poly.thy	Wed Nov 28 11:46:00 2018 +0100
    14.3 @@ -1618,7 +1618,7 @@
    14.4  
    14.5  -----*)
    14.6  setup \<open>KEStore_Elems.add_mets
    14.7 -  [Specify.prep_met thy "met_simp_poly" [] Celem.e_metID
    14.8 +    [Specify.prep_met thy "met_simp_poly" [] Celem.e_metID
    14.9  	    (["simplification","for_polynomials"],
   14.10  	      [("#Given" ,["Term t_t"]),
   14.11  	        ("#Where" ,["t_t is_polyexp"]),

    15.1 --- a/src/Tools/isac/Knowledge/PolyEq.thy	Wed Nov 21 12:32:54 2018 +0100
    15.2 +++ b/src/Tools/isac/Knowledge/PolyEq.thy	Wed Nov 28 11:46:00 2018 +0100
    15.3 @@ -968,12 +968,14 @@
    15.4  
    15.5  text \<open>"-------------------------methods-----------------------"\<close>
    15.6  setup \<open>KEStore_Elems.add_mets
    15.7 -  [Specify.prep_met thy "met_polyeq" [] Celem.e_metID
    15.8 +    [Specify.prep_met thy "met_polyeq" [] Celem.e_metID
    15.9        (["PolyEq"], [],
   15.10          {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = Rule.e_rls, prls=Rule.e_rls,
   15.11            crls=PolyEq_crls, errpats = [], nrls = norm_Rational},
   15.12 -        "empty_script"),
   15.13 -    Specify.prep_met thy "met_polyeq_norm" [] Celem.e_metID
   15.14 +        "empty_script")]
   15.15 +\<close>
   15.16 +setup \<open>KEStore_Elems.add_mets
   15.17 +    [Specify.prep_met thy "met_polyeq_norm" [] Celem.e_metID
   15.18        (["PolyEq","normalise_poly"],
   15.19          [("#Given" ,["equality e_e","solveFor v_v"]),
   15.20            ("#Where" ,["(Not((matches (?a = 0 ) e_e ))) |(Not(((lhs e_e) is_poly_in v_v)))"]),
   15.21 @@ -988,8 +990,10 @@
   15.22            "                                 make_ratpoly_in     False))) @@  " ^
   15.23            "          (Try (Repeat (Rewrite_Set polyeq_simplify  False)))) e_e " ^
   15.24            " in (SubProblem (PolyEq',[polynomial,univariate,equation], [no_met])   " ^
   15.25 -          "                 [BOOL e_e, REAL v_v]))"),
   15.26 -    Specify.prep_met thy "met_polyeq_d0" [] Celem.e_metID
   15.27 +          "                 [BOOL e_e, REAL v_v]))")]
   15.28 +\<close>
   15.29 +setup \<open>KEStore_Elems.add_mets
   15.30 +    [Specify.prep_met thy "met_polyeq_d0" [] Celem.e_metID
   15.31        (["PolyEq","solve_d0_polyeq_equation"],
   15.32          [("#Given" ,["equality e_e","solveFor v_v"]),
   15.33            ("#Where" ,["(lhs e_e) is_poly_in v_v ", "((lhs e_e) has_degree_in v_v) = 0"]),
   15.34 @@ -1000,8 +1004,10 @@
   15.35          "Script Solve_d0_polyeq_equation  (e_e::bool) (v_v::real)  = " ^
   15.36            "(let e_e =  ((Try (Rewrite_Set_Inst [(bdv,v_v::real)]      " ^
   15.37            "                  d0_polyeq_simplify  False))) e_e        " ^
   15.38 -          " in ((Or_to_List e_e)::bool list))"),
   15.39 -    Specify.prep_met thy "met_polyeq_d1" [] Celem.e_metID
   15.40 +          " in ((Or_to_List e_e)::bool list))")]
   15.41 +\<close>
   15.42 +setup \<open>KEStore_Elems.add_mets
   15.43 +    [Specify.prep_met thy "met_polyeq_d1" [] Celem.e_metID
   15.44        (["PolyEq","solve_d1_polyeq_equation"],
   15.45          [("#Given" ,["equality e_e","solveFor v_v"]),
   15.46            ("#Where" ,["(lhs e_e) is_poly_in v_v ", "((lhs e_e) has_degree_in v_v) = 1"]),
   15.47 @@ -1015,8 +1021,10 @@
   15.48            "            (Try (Rewrite_Set polyeq_simplify  False)) @@  " ^
   15.49            "            (Try (Rewrite_Set norm_Rational_parenthesized False))) e_e;" ^
   15.50            " (L_L::bool list) = ((Or_to_List e_e)::bool list)            " ^
   15.51 -          " in Check_elementwise L_L {(v_v::real). Assumptions} )"),
   15.52 -    Specify.prep_met thy "met_polyeq_d22" [] Celem.e_metID
   15.53 +          " in Check_elementwise L_L {(v_v::real). Assumptions} )")]
   15.54 +\<close>
   15.55 +setup \<open>KEStore_Elems.add_mets
   15.56 +    [Specify.prep_met thy "met_polyeq_d22" [] Celem.e_metID
   15.57        (["PolyEq","solve_d2_polyeq_equation"],
   15.58          [("#Given" ,["equality e_e","solveFor v_v"]),
   15.59            ("#Where" ,["(lhs e_e) is_poly_in v_v ", "((lhs e_e) has_degree_in v_v) = 2"]),
   15.60 @@ -1033,8 +1041,10 @@
   15.61              "            (Try (Rewrite_Set polyeq_simplify    False)) @@  " ^
   15.62              "            (Try (Rewrite_Set norm_Rational_parenthesized False))) e_e;" ^
   15.63              " (L_L::bool list) = ((Or_to_List e_e)::bool list)              " ^
   15.64 -            " in Check_elementwise L_L {(v_v::real). Assumptions} )"),
   15.65 -    Specify.prep_met thy "met_polyeq_d2_bdvonly" [] Celem.e_metID
   15.66 +            " in Check_elementwise L_L {(v_v::real). Assumptions} )")]
   15.67 +\<close>
   15.68 +setup \<open>KEStore_Elems.add_mets
   15.69 +    [Specify.prep_met thy "met_polyeq_d2_bdvonly" [] Celem.e_metID
   15.70        (["PolyEq","solve_d2_polyeq_bdvonly_equation"],
   15.71          [("#Given" ,["equality e_e","solveFor v_v"]),
   15.72            ("#Where" ,["(lhs e_e) is_poly_in v_v ", "((lhs e_e) has_degree_in v_v) = 2"]),
   15.73 @@ -1051,8 +1061,10 @@
   15.74              "            (Try (Rewrite_Set polyeq_simplify    False)) @@  " ^
   15.75              "            (Try (Rewrite_Set norm_Rational_parenthesized False))) e_e;" ^
   15.76              " (L_L::bool list) = ((Or_to_List e_e)::bool list)              " ^
   15.77 -            " in Check_elementwise L_L {(v_v::real). Assumptions} )"),
   15.78 -    Specify.prep_met thy "met_polyeq_d2_sqonly" [] Celem.e_metID
   15.79 +            " in Check_elementwise L_L {(v_v::real). Assumptions} )")]
   15.80 +\<close>
   15.81 +setup \<open>KEStore_Elems.add_mets
   15.82 +    [Specify.prep_met thy "met_polyeq_d2_sqonly" [] Celem.e_metID
   15.83        (["PolyEq","solve_d2_polyeq_sqonly_equation"],
   15.84          [("#Given" ,["equality e_e","solveFor v_v"]),
   15.85            ("#Where" ,["(lhs e_e) is_poly_in v_v ", "((lhs e_e) has_degree_in v_v) = 2"]),
   15.86 @@ -1066,8 +1078,10 @@
   15.87              "            (Try (Rewrite_Set polyeq_simplify    False)) @@   " ^
   15.88              "            (Try (Rewrite_Set norm_Rational_parenthesized False))) e_e; " ^
   15.89              " (L_L::bool list) = ((Or_to_List e_e)::bool list)               " ^
   15.90 -            " in Check_elementwise L_L {(v_v::real). Assumptions} )"),
   15.91 -    Specify.prep_met thy "met_polyeq_d2_pq" [] Celem.e_metID
   15.92 +            " in Check_elementwise L_L {(v_v::real). Assumptions} )")]
   15.93 +\<close>
   15.94 +setup \<open>KEStore_Elems.add_mets
   15.95 +    [Specify.prep_met thy "met_polyeq_d2_pq" [] Celem.e_metID
   15.96        (["PolyEq","solve_d2_polyeq_pq_equation"],
   15.97          [("#Given" ,["equality e_e","solveFor v_v"]),
   15.98            ("#Where" ,["(lhs e_e) is_poly_in v_v ", "((lhs e_e) has_degree_in v_v) = 2"]),
   15.99 @@ -1081,8 +1095,10 @@
  15.100              "            (Try (Rewrite_Set polyeq_simplify    False)) @@  " ^
  15.101              "            (Try (Rewrite_Set norm_Rational_parenthesized False))) e_e;" ^
  15.102              " (L_L::bool list) = ((Or_to_List e_e)::bool list)              " ^
  15.103 -            " in Check_elementwise L_L {(v_v::real). Assumptions} )"),
  15.104 -    Specify.prep_met thy "met_polyeq_d2_abc" [] Celem.e_metID
  15.105 +            " in Check_elementwise L_L {(v_v::real). Assumptions} )")]
  15.106 +\<close>
  15.107 +setup \<open>KEStore_Elems.add_mets
  15.108 +    [Specify.prep_met thy "met_polyeq_d2_abc" [] Celem.e_metID
  15.109        (["PolyEq","solve_d2_polyeq_abc_equation"],
  15.110          [("#Given" ,["equality e_e","solveFor v_v"]),
  15.111            ("#Where" ,["(lhs e_e) is_poly_in v_v ", "((lhs e_e) has_degree_in v_v) = 2"]),
  15.112 @@ -1096,8 +1112,10 @@
  15.113              "            (Try (Rewrite_Set polyeq_simplify     False)) @@  " ^
  15.114              "            (Try (Rewrite_Set norm_Rational_parenthesized False))) e_e;" ^
  15.115              " (L_L::bool list) = ((Or_to_List e_e)::bool list)               " ^
  15.116 -            " in Check_elementwise L_L {(v_v::real). Assumptions} )"),
  15.117 -    Specify.prep_met thy "met_polyeq_d3" [] Celem.e_metID
  15.118 +            " in Check_elementwise L_L {(v_v::real). Assumptions} )")]
  15.119 +\<close>
  15.120 +setup \<open>KEStore_Elems.add_mets
  15.121 +    [Specify.prep_met thy "met_polyeq_d3" [] Celem.e_metID
  15.122        (["PolyEq","solve_d3_polyeq_equation"],
  15.123          [("#Given" ,["equality e_e","solveFor v_v"]),
  15.124            ("#Where" ,["(lhs e_e) is_poly_in v_v ", "((lhs e_e) has_degree_in v_v) = 3"]),
  15.125 @@ -1117,11 +1135,13 @@
  15.126            "             (Try (Rewrite_Set polyeq_simplify  False)) @@  " ^
  15.127            "             (Try (Rewrite_Set norm_Rational_parenthesized False))) e_e;" ^
  15.128            " (L_L::bool list) = ((Or_to_List e_e)::bool list)             " ^
  15.129 -          " in Check_elementwise L_L {(v_v::real). Assumptions} )"),
  15.130 +          " in Check_elementwise L_L {(v_v::real). Assumptions} )")]
  15.131 +\<close>
  15.132      (*.solves all expanded (ie. normalised) terms of degree 2.*) 
  15.133      (*Oct.02 restriction: 'eval_true 0 =< discriminant' ony for integer values
  15.134        by 'PolyEq_erls'; restricted until Float.thy is implemented*)
  15.135 -    Specify.prep_met thy "met_polyeq_complsq" [] Celem.e_metID
  15.136 +setup \<open>KEStore_Elems.add_mets
  15.137 +    [Specify.prep_met thy "met_polyeq_complsq" [] Celem.e_metID
  15.138        (["PolyEq","complete_square"],
  15.139          [("#Given" ,["equality e_e","solveFor v_v"]),
  15.140            ("#Where" ,["matches (?a = 0) e_e", "((lhs e_e) has_degree_in v_v) = 2"]),

    16.1 --- a/src/Tools/isac/Knowledge/PolyMinus.thy	Wed Nov 21 12:32:54 2018 +0100
    16.2 +++ b/src/Tools/isac/Knowledge/PolyMinus.thy	Wed Nov 28 11:46:00 2018 +0100
    16.3 @@ -476,7 +476,7 @@
    16.4  
    16.5  (** methods **)
    16.6  setup \<open>KEStore_Elems.add_mets
    16.7 -  [Specify.prep_met thy "met_simp_poly_minus" [] Celem.e_metID
    16.8 +    [Specify.prep_met thy "met_simp_poly_minus" [] Celem.e_metID
    16.9  	    (["simplification","for_polynomials","with_minus"],
   16.10  	      [("#Given" ,["Term t_t"]),
   16.11  	        ("#Where" ,["t_t is_polyexp",
   16.12 @@ -501,8 +501,10 @@
   16.13            "Script SimplifyScript (t_t::real) =                   " ^
   16.14              "  ((Repeat((Try (Rewrite_Set ordne_alphabetisch False)) @@  " ^
   16.15              "           (Try (Rewrite_Set fasse_zusammen     False)) @@  " ^
   16.16 -            "           (Try (Rewrite_Set verschoenere       False)))) t_t)"),
   16.17 -    Specify.prep_met thy "met_simp_poly_parenth" [] Celem.e_metID
   16.18 +            "           (Try (Rewrite_Set verschoenere       False)))) t_t)")]
   16.19 +\<close>
   16.20 +setup \<open>KEStore_Elems.add_mets
   16.21 +    [Specify.prep_met thy "met_simp_poly_parenth" [] Celem.e_metID
   16.22  	    (["simplification","for_polynomials","with_parentheses"],
   16.23  	      [("#Given" ,["Term t_t"]),
   16.24  	        ("#Where" ,["t_t is_polyexp"]),
   16.25 @@ -515,8 +517,10 @@
   16.26            "  ((Repeat((Try (Rewrite_Set klammern_aufloesen False)) @@  " ^
   16.27            "           (Try (Rewrite_Set ordne_alphabetisch False)) @@  " ^
   16.28            "           (Try (Rewrite_Set fasse_zusammen     False)) @@  " ^
   16.29 -          "           (Try (Rewrite_Set verschoenere       False)))) t_t)"),
   16.30 -    Specify.prep_met thy "met_simp_poly_parenth_mult" [] Celem.e_metID
   16.31 +          "           (Try (Rewrite_Set verschoenere       False)))) t_t)")]
   16.32 +\<close>
   16.33 +setup \<open>KEStore_Elems.add_mets
   16.34 +    [Specify.prep_met thy "met_simp_poly_parenth_mult" [] Celem.e_metID
   16.35  	    (["simplification","for_polynomials","with_parentheses_mult"],
   16.36  	      [("#Given" ,["Term t_t"]), ("#Where" ,["t_t is_polyexp"]), ("#Find"  ,["normalform n_n"])],
   16.37  	        {rew_ord'="tless_true", rls' = Rule.e_rls, calc = [], srls = Rule.e_rls, 
   16.38 @@ -530,13 +534,17 @@
   16.39              "           (Try (Rewrite_Set klammern_aufloesen         False)) @@ " ^
   16.40              "           (Try (Rewrite_Set ordne_alphabetisch         False)) @@ " ^
   16.41              "           (Try (Rewrite_Set fasse_zusammen             False)) @@ " ^
   16.42 -            "           (Try (Rewrite_Set verschoenere               False)))) t_t)"),
   16.43 -    Specify.prep_met thy "met_probe" [] Celem.e_metID
   16.44 +            "           (Try (Rewrite_Set verschoenere               False)))) t_t)")]
   16.45 +\<close>
   16.46 +setup \<open>KEStore_Elems.add_mets
   16.47 +    [Specify.prep_met thy "met_probe" [] Celem.e_metID
   16.48  	    (["probe"], [],
   16.49  	      {rew_ord'="tless_true", rls' = Rule.e_rls, calc = [], srls = Rule.e_rls, prls = Rule.Erls, crls = Rule.e_rls,
   16.50  	        errpats = [], nrls = Rule.Erls}, 
   16.51 -	      "empty_script"),
   16.52 -    Specify.prep_met thy "met_probe_poly" [] Celem.e_metID
   16.53 +	      "empty_script")]
   16.54 +\<close>
   16.55 +setup \<open>KEStore_Elems.add_mets
   16.56 +    [Specify.prep_met thy "met_probe_poly" [] Celem.e_metID
   16.57  	    (["probe","fuer_polynom"],
   16.58  	      [("#Given" ,["Pruefe e_e", "mitWert w_w"]),
   16.59  	        ("#Where" ,["e_e is_polyexp"]),
   16.60 @@ -550,8 +558,10 @@
   16.61            "      e_e = Substitute w_w e_e                     " ^
   16.62            " in (Repeat((Try (Repeat (Calculate TIMES))) @@  " ^
   16.63            "            (Try (Repeat (Calculate PLUS ))) @@  " ^
   16.64 -          "            (Try (Repeat (Calculate MINUS))))) e_e)"),
   16.65 -    Specify.prep_met thy "met_probe_bruch" [] Celem.e_metID
   16.66 +          "            (Try (Repeat (Calculate MINUS))))) e_e)")]
   16.67 +\<close>
   16.68 +setup \<open>KEStore_Elems.add_mets
   16.69 +    [Specify.prep_met thy "met_probe_bruch" [] Celem.e_metID
   16.70  	    (["probe","fuer_bruch"],
   16.71  	      [("#Given" ,["Pruefe e_e", "mitWert w_w"]),
   16.72  	        ("#Where" ,["e_e is_ratpolyexp"]),

    17.1 --- a/src/Tools/isac/Knowledge/RatEq.thy	Wed Nov 21 12:32:54 2018 +0100
    17.2 +++ b/src/Tools/isac/Knowledge/RatEq.thy	Wed Nov 28 11:46:00 2018 +0100
    17.3 @@ -192,11 +192,13 @@
    17.4  
    17.5  (*-------------------------methods-----------------------*)
    17.6  setup \<open>KEStore_Elems.add_mets
    17.7 -  [Specify.prep_met thy "met_rateq" [] Celem.e_metID
    17.8 +    [Specify.prep_met thy "met_rateq" [] Celem.e_metID
    17.9        (["RatEq"], [],
   17.10          {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = Rule.e_rls, prls=Rule.e_rls,
   17.11 -          crls=RatEq_crls, errpats = [], nrls = norm_Rational}, "empty_script"),
   17.12 -    Specify.prep_met thy "met_rat_eq" [] Celem.e_metID
   17.13 +          crls=RatEq_crls, errpats = [], nrls = norm_Rational}, "empty_script")]
   17.14 +\<close>
   17.15 +setup \<open>KEStore_Elems.add_mets
   17.16 +    [Specify.prep_met thy "met_rat_eq" [] Celem.e_metID
   17.17        (["RatEq", "solve_rat_equation"],
   17.18          [("#Given" ,["equality e_e","solveFor v_v"]),
   17.19            ("#Where" ,["(e_e::bool) is_ratequation_in (v_v::real)"]),

    18.1 --- a/src/Tools/isac/Knowledge/Rational.thy	Wed Nov 21 12:32:54 2018 +0100
    18.2 +++ b/src/Tools/isac/Knowledge/Rational.thy	Wed Nov 28 11:46:00 2018 +0100
    18.3 @@ -898,7 +898,7 @@
    18.4  (*WN061025 this methods script is copied from (auto-generated) script
    18.5    of norm_Rational in order to ease repair on inform*)
    18.6  setup \<open>KEStore_Elems.add_mets
    18.7 -  [Specify.prep_met thy "met_simp_rat" [] Celem.e_metID
    18.8 +    [Specify.prep_met thy "met_simp_rat" [] Celem.e_metID
    18.9        (["simplification","of_rationals"],
   18.10          [("#Given" ,["Term t_t"]),
   18.11            ("#Where" ,["t_t is_ratpolyexp"]),

    19.1 --- a/src/Tools/isac/Knowledge/RootEq.thy	Wed Nov 21 12:32:54 2018 +0100
    19.2 +++ b/src/Tools/isac/Knowledge/RootEq.thy	Wed Nov 28 11:46:00 2018 +0100
    19.3 @@ -515,13 +515,14 @@
    19.4  
    19.5  (*-------------------------methods-----------------------*)
    19.6  setup \<open>KEStore_Elems.add_mets
    19.7 -  [(* ---- root 20.8.02 ---*)
    19.8 -    Specify.prep_met thy "met_rooteq" [] Celem.e_metID
    19.9 +    [Specify.prep_met thy "met_rooteq" [] Celem.e_metID
   19.10        (["RootEq"], [],
   19.11          {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = Rule.e_rls, prls=Rule.e_rls,
   19.12 -          crls=RootEq_crls, errpats = [], nrls = norm_Poly}, "empty_script"),
   19.13 +          crls=RootEq_crls, errpats = [], nrls = norm_Poly}, "empty_script")]
   19.14 +\<close>
   19.15      (*-- normalise 20.10.02 --*)
   19.16 -    Specify.prep_met thy "met_rooteq_norm" [] Celem.e_metID
   19.17 +setup \<open>KEStore_Elems.add_mets
   19.18 +    [Specify.prep_met thy "met_rooteq_norm" [] Celem.e_metID
   19.19        (["RootEq","norm_sq_root_equation"],
   19.20          [("#Given" ,["equality e_e","solveFor v_v"]),
   19.21            ("#Where" ,["( ((lhs e_e) is_sqrtTerm_in (v_v::real)) &" ^
   19.22 @@ -538,8 +539,10 @@
   19.23            "           (Try (Repeat (Rewrite_Set make_rooteq        False))) @@  " ^
   19.24            "           (Try (Rewrite_Set rooteq_simplify              True))) e_e " ^
   19.25            " in ((SubProblem (RootEq',[univariate,equation],                     " ^
   19.26 -          "      [no_met]) [BOOL e_e, REAL v_v])))"),
   19.27 -    Specify.prep_met thy "met_rooteq_sq" [] Celem.e_metID
   19.28 +          "      [no_met]) [BOOL e_e, REAL v_v])))")]
   19.29 +\<close>
   19.30 +setup \<open>KEStore_Elems.add_mets
   19.31 +    [Specify.prep_met thy "met_rooteq_sq" [] Celem.e_metID
   19.32        (["RootEq","solve_sq_root_equation"],
   19.33          [("#Given" ,["equality e_e", "solveFor v_v"]),
   19.34            ("#Where" ,["(((lhs e_e) is_sqrtTerm_in (v_v::real))     & " ^
   19.35 @@ -562,9 +565,11 @@
   19.36            "                      [no_met]) [BOOL e_e, REAL v_v])                   " ^
   19.37            "    else (SubProblem (RootEq',[univariate,equation], [no_met])         " ^
   19.38            "                     [BOOL e_e, REAL v_v]))                             " ^
   19.39 -          "in Check_elementwise L_L {(v_v::real). Assumptions})"),
   19.40 +          "in Check_elementwise L_L {(v_v::real). Assumptions})")]
   19.41 +\<close>
   19.42      (*-- right 28.08.02 --*)
   19.43 -    Specify.prep_met thy "met_rooteq_sq_right" [] Celem.e_metID
   19.44 +setup \<open>KEStore_Elems.add_mets
   19.45 +    [Specify.prep_met thy "met_rooteq_sq_right" [] Celem.e_metID
   19.46        (["RootEq","solve_right_sq_root_equation"],
   19.47          [("#Given" ,["equality e_e","solveFor v_v"]),
   19.48            ("#Where" ,["(rhs e_e) is_sqrtTerm_in v_v"]),
   19.49 @@ -582,9 +587,11 @@
   19.50            " then (SubProblem (RootEq',[normalise,root',univariate,equation],       " ^
   19.51            "       [no_met]) [BOOL e_e, REAL v_v])                                   " ^
   19.52            " else ((SubProblem (RootEq',[univariate,equation],                      " ^
   19.53 -          "        [no_met]) [BOOL e_e, REAL v_v])))"),
   19.54 +          "        [no_met]) [BOOL e_e, REAL v_v])))")]
   19.55 +\<close>
   19.56      (*-- left 28.08.02 --*)
   19.57 -    Specify.prep_met thy "met_rooteq_sq_left" [] Celem.e_metID
   19.58 +setup \<open>KEStore_Elems.add_mets
   19.59 +    [Specify.prep_met thy "met_rooteq_sq_left" [] Celem.e_metID
   19.60        (["RootEq","solve_left_sq_root_equation"],
   19.61          [("#Given" ,["equality e_e","solveFor v_v"]),
   19.62            ("#Where" ,["(lhs e_e) is_sqrtTerm_in v_v"]),
   19.63 @@ -602,7 +609,8 @@
   19.64            " then (SubProblem (RootEq',[normalise,root',univariate,equation],      " ^
   19.65            "       [no_met]) [BOOL e_e, REAL v_v])                                " ^
   19.66            " else ((SubProblem (RootEq',[univariate,equation],                    " ^
   19.67 -          "        [no_met]) [BOOL e_e, REAL v_v])))")]\<close>
   19.68 +          "        [no_met]) [BOOL e_e, REAL v_v])))")]
   19.69 +\<close>
   19.70  
   19.71  setup \<open>KEStore_Elems.add_calcs
   19.72    [("is_rootTerm_in", ("RootEq.is'_rootTerm'_in", eval_is_rootTerm_in"")),

    20.1 --- a/src/Tools/isac/Knowledge/RootRatEq.thy	Wed Nov 21 12:32:54 2018 +0100
    20.2 +++ b/src/Tools/isac/Knowledge/RootRatEq.thy	Wed Nov 28 11:46:00 2018 +0100
    20.3 @@ -149,12 +149,14 @@
    20.4  
    20.5  (*-------------------------Methode-----------------------*)
    20.6  setup \<open>KEStore_Elems.add_mets
    20.7 -  [Specify.prep_met @{theory LinEq} "met_rootrateq" [] Celem.e_metID
    20.8 +    [Specify.prep_met @{theory LinEq} "met_rootrateq" [] Celem.e_metID
    20.9        (["RootRatEq"], [],
   20.10          {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = Rule.e_rls, prls=Rule.e_rls,
   20.11 -          crls=Atools_erls, errpats = [], nrls = norm_Rational}, "empty_script"),
   20.12 +          crls=Atools_erls, errpats = [], nrls = norm_Rational}, "empty_script")]
   20.13 +\<close>
   20.14      (*-- left 20.10.02 --*)
   20.15 -    Specify.prep_met thy "met_rootrateq_elim" [] Celem.e_metID
   20.16 +setup \<open>KEStore_Elems.add_mets
   20.17 +    [Specify.prep_met thy "met_rootrateq_elim" [] Celem.e_metID
   20.18        (["RootRatEq","elim_rootrat_equation"],
   20.19          [("#Given" ,["equality e_e","solveFor v_v"]),
   20.20            ("#Where" ,["( (lhs e_e) is_rootRatAddTerm_in (v_v::real) ) | " ^

    21.1 --- a/src/Tools/isac/Knowledge/Simplify.thy	Wed Nov 21 12:32:54 2018 +0100
    21.2 +++ b/src/Tools/isac/Knowledge/Simplify.thy	Wed Nov 28 11:46:00 2018 +0100
    21.3 @@ -42,7 +42,7 @@
    21.4  
    21.5  (** methods **)
    21.6  setup \<open>KEStore_Elems.add_mets
    21.7 -  [Specify.prep_met thy "met_tsimp" [] Celem.e_metID
    21.8 +    [Specify.prep_met thy "met_tsimp" [] Celem.e_metID
    21.9  	    (["simplification"],
   21.10  	      [("#Given" ,["Term t_t"]),
   21.11  		      ("#Find"  ,["normalform n_n"])],

    22.1 --- a/src/Tools/isac/Knowledge/Test.thy	Wed Nov 21 12:32:54 2018 +0100
    22.2 +++ b/src/Tools/isac/Knowledge/Test.thy	Wed Nov 28 11:46:00 2018 +0100
    22.3 @@ -864,11 +864,13 @@
    22.4  partial_function (tailrec) dummy1 :: "real \<Rightarrow> real"
    22.5    where "dummy1 xxx = xxx"
    22.6  setup \<open>KEStore_Elems.add_mets
    22.7 -  [Specify.prep_met @{theory "Diff"} "met_test" [] Celem.e_metID
    22.8 +    [Specify.prep_met @{theory "Diff"} "met_test" [] Celem.e_metID
    22.9        (["Test"], [],
   22.10          {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = Rule.e_rls, prls=Rule.e_rls,
   22.11 -          crls=Atools_erls, errpats = [], nrls = Rule.e_rls}, "empty_script"),
   22.12 -    Specify.prep_met thy "met_test_solvelin" [] Celem.e_metID
   22.13 +          crls=Atools_erls, errpats = [], nrls = Rule.e_rls}, "empty_script")]
   22.14 +\<close>
   22.15 +setup \<open>KEStore_Elems.add_mets
   22.16 +    [Specify.prep_met thy "met_test_solvelin" [] Celem.e_metID
   22.17        (["Test","solve_linear"],
   22.18          [("#Given" ,["equality e_e","solveFor v_v"]),
   22.19            ("#Where" ,["matches (?a = ?b) e_e"]),
   22.20 @@ -887,7 +889,7 @@
   22.21  partial_function (tailrec) dummy2 :: "real \<Rightarrow> real"
   22.22    where "dummy2 xxx = xxx"
   22.23  setup \<open>KEStore_Elems.add_mets
   22.24 -  [Specify.prep_met thy  "met_test_sqrt" [] Celem.e_metID
   22.25 +    [Specify.prep_met thy  "met_test_sqrt" [] Celem.e_metID
   22.26        (*root-equation, version for tests before 8.01.01*)
   22.27        (["Test","sqrt-equ-test"],
   22.28          [("#Given" ,["equality e_e","solveFor v_v"]),
   22.29 @@ -918,7 +920,7 @@
   22.30  partial_function (tailrec) dummy3 :: "real \<Rightarrow> real"
   22.31    where "dummy3 xxx = xxx"
   22.32  setup \<open>KEStore_Elems.add_mets
   22.33 -  [Specify.prep_met thy  "met_test_sqrt2" [] Celem.e_metID
   22.34 +    [Specify.prep_met thy  "met_test_sqrt2" [] Celem.e_metID
   22.35        (*root-equation ... for test-*.sml until 8.01*)
   22.36        (["Test","squ-equ-test2"],
   22.37          [("#Given" ,["equality e_e","solveFor v_v"]),
   22.38 @@ -948,7 +950,7 @@
   22.39  partial_function (tailrec) dummy4 :: "real \<Rightarrow> real"
   22.40    where "dummy4 xxx = xxx"
   22.41  setup \<open>KEStore_Elems.add_mets
   22.42 -  [Specify.prep_met thy "met_test_squ_sub" [] Celem.e_metID
   22.43 +    [Specify.prep_met thy "met_test_squ_sub" [] Celem.e_metID
   22.44        (*tests subproblem fixed linear*)
   22.45        (["Test","squ-equ-test-subpbl1"],
   22.46          [("#Given" ,["equality e_e","solveFor v_v"]),
   22.47 @@ -971,7 +973,7 @@
   22.48  partial_function (tailrec) dummy5 :: "real \<Rightarrow> real"
   22.49    where "dummy5 xxx = xxx"
   22.50  setup \<open>KEStore_Elems.add_mets
   22.51 -  [Specify.prep_met thy "met_test_squ_sub2" [] Celem.e_metID
   22.52 +    [Specify.prep_met thy "met_test_squ_sub2" [] Celem.e_metID
   22.53        (*tests subproblem fixed degree 2*)
   22.54        (["Test","squ-equ-test-subpbl2"],
   22.55          [("#Given" ,["equality e_e","solveFor v_v"]),
   22.56 @@ -988,7 +990,7 @@
   22.57  partial_function (tailrec) dummy7 :: "real \<Rightarrow> real"
   22.58    where "dummy7 xxx = xxx"
   22.59  setup \<open>KEStore_Elems.add_mets
   22.60 -  [Specify.prep_met thy  "met_test_eq1" [] Celem.e_metID
   22.61 +    [Specify.prep_met thy  "met_test_eq1" [] Celem.e_metID
   22.62        (*root-equation1:*)
   22.63        (["Test","square_equation1"],
   22.64          [("#Given" ,["equality e_e","solveFor v_v"]),
   22.65 @@ -1016,7 +1018,7 @@
   22.66  partial_function (tailrec) dummy8 :: "real \<Rightarrow> real"
   22.67    where "dummy8 xxx = xxx"
   22.68  setup \<open>KEStore_Elems.add_mets
   22.69 -  [Specify.prep_met thy "met_test_squ2" [] Celem.e_metID
   22.70 +    [Specify.prep_met thy "met_test_squ2" [] Celem.e_metID
   22.71        (*root-equation2*)
   22.72          (["Test","square_equation2"],
   22.73            [("#Given" ,["equality e_e","solveFor v_v"]),
   22.74 @@ -1045,7 +1047,7 @@
   22.75  partial_function (tailrec) dummy9 :: "real \<Rightarrow> real"
   22.76    where "dummy9 xxx = xxx"
   22.77  setup \<open>KEStore_Elems.add_mets
   22.78 -  [Specify.prep_met thy "met_test_squeq" [] Celem.e_metID
   22.79 +    [Specify.prep_met thy "met_test_squeq" [] Celem.e_metID
   22.80        (*root-equation*)
   22.81        (["Test","square_equation"],
   22.82          [("#Given" ,["equality e_e","solveFor v_v"]),
   22.83 @@ -1074,7 +1076,7 @@
   22.84  partial_function (tailrec) dummy10 :: "real \<Rightarrow> real"
   22.85    where "dummy10 xxx = xxx"
   22.86  setup \<open>KEStore_Elems.add_mets
   22.87 -  [Specify.prep_met thy "met_test_eq_plain" [] Celem.e_metID
   22.88 +    [Specify.prep_met thy "met_test_eq_plain" [] Celem.e_metID
   22.89        (*solve_plain_square*)
   22.90        (["Test","solve_plain_square"],
   22.91          [("#Given",["equality e_e","solveFor v_v"]),
   22.92 @@ -1098,7 +1100,7 @@
   22.93  partial_function (tailrec) dummy11 :: "real \<Rightarrow> real"
   22.94    where "dummy11 xxx = xxx"
   22.95  setup \<open>KEStore_Elems.add_mets
   22.96 -  [Specify.prep_met thy "met_test_norm_univ" [] Celem.e_metID
   22.97 +    [Specify.prep_met thy "met_test_norm_univ" [] Celem.e_metID
   22.98        (["Test","norm_univar_equation"],
   22.99          [("#Given",["equality e_e","solveFor v_v"]),
  22.100            ("#Where" ,[]), 
  22.101 @@ -1115,7 +1117,7 @@
  22.102  partial_function (tailrec) dummy12 :: "real \<Rightarrow> real"
  22.103    where "dummy12 xxx = xxx"
  22.104  setup \<open>KEStore_Elems.add_mets
  22.105 -  [Specify.prep_met thy "met_test_intsimp" [] Celem.e_metID
  22.106 +    [Specify.prep_met thy "met_test_intsimp" [] Celem.e_metID
  22.107        (["Test","intsimp"],
  22.108          [("#Given" ,["intTestGiven t_t"]),
  22.109            ("#Where" ,[]),

    23.1 --- a/src/Tools/isac/calcelems.sml	Wed Nov 21 12:32:54 2018 +0100
    23.2 +++ b/src/Tools/isac/calcelems.sml	Wed Nov 28 11:46:00 2018 +0100
    23.3 @@ -636,7 +636,7 @@
    23.4  fun check_metguh_unique (guh:guh) (mets: (met ptyp) list) =
    23.5      if member op = (coll_metguhs mets) guh
    23.6      then raise ERROR ("check_guh_unique failed with \"" ^ guh ^"\";\n"^
    23.7 -		  "use \"sort_metguhs()\" for a list of guhs;\n" ^
    23.8 +		(*"use \"sort_metguhs()\" for a list of guhs;\n" ^        ...evaluates to [] ?!?*)
    23.9  		  "consider setting \"check_guhs_unique := false\"")
   23.10      else ();
   23.11