1.1 --- a/src/Tools/isac/Knowledge/PolyEq.thy	Wed Feb 03 15:21:12 2021 +0100
     1.2 +++ b/src/Tools/isac/Knowledge/PolyEq.thy	Wed Feb 03 16:39:44 2021 +0100
     1.3 @@ -901,7 +901,7 @@
     1.4  
     1.5  text \<open>"-------------------------methods-----------------------"\<close>
     1.6  setup \<open>KEStore_Elems.add_mets
     1.7 -    [Method.prep_input thy "met_polyeq" [] Method.id_empty
     1.8 +    [MethodC.prep_input thy "met_polyeq" [] MethodC.id_empty
     1.9        (["PolyEq"], [],
    1.10          {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty,
    1.11            crls=PolyEq_crls, errpats = [], nrls = norm_Rational},
    1.12 @@ -922,7 +922,7 @@
    1.13      SubProblem (''PolyEq'', [''polynomial'', ''univariate'', ''equation''], [''no_met''])
    1.14        [BOOL e_e, REAL v_v])"
    1.15  setup \<open>KEStore_Elems.add_mets
    1.16 -    [Method.prep_input thy "met_polyeq_norm" [] Method.id_empty
    1.17 +    [MethodC.prep_input thy "met_polyeq_norm" [] MethodC.id_empty
    1.18        (["PolyEq", "normalise_poly"],
    1.19          [("#Given" ,["equality e_e", "solveFor v_v"]),
    1.20            ("#Where" ,["(Not((matches (?a = 0 ) e_e ))) | (Not(((lhs e_e) is_poly_in v_v)))"]),
    1.21 @@ -940,7 +940,7 @@
    1.22    in
    1.23      Or_to_List e_e)"
    1.24  setup \<open>KEStore_Elems.add_mets
    1.25 -    [Method.prep_input thy "met_polyeq_d0" [] Method.id_empty
    1.26 +    [MethodC.prep_input thy "met_polyeq_d0" [] MethodC.id_empty
    1.27        (["PolyEq", "solve_d0_polyeq_equation"],
    1.28          [("#Given" ,["equality e_e", "solveFor v_v"]),
    1.29            ("#Where" ,["(lhs e_e) is_poly_in v_v ", "((lhs e_e) has_degree_in v_v) = 0"]),
    1.30 @@ -963,7 +963,7 @@
    1.31    in
    1.32      Check_elementwise L_L {(v_v::real). Assumptions})"
    1.33  setup \<open>KEStore_Elems.add_mets
    1.34 -    [Method.prep_input thy "met_polyeq_d1" [] Method.id_empty
    1.35 +    [MethodC.prep_input thy "met_polyeq_d1" [] MethodC.id_empty
    1.36        (["PolyEq", "solve_d1_polyeq_equation"],
    1.37          [("#Given" ,["equality e_e", "solveFor v_v"]),
    1.38            ("#Where" ,["(lhs e_e) is_poly_in v_v ", "((lhs e_e) has_degree_in v_v) = 1"]),
    1.39 @@ -988,7 +988,7 @@
    1.40    in
    1.41      Check_elementwise L_L {(v_v::real). Assumptions})"
    1.42  setup \<open>KEStore_Elems.add_mets
    1.43 -    [Method.prep_input thy "met_polyeq_d22" [] Method.id_empty
    1.44 +    [MethodC.prep_input thy "met_polyeq_d22" [] MethodC.id_empty
    1.45        (["PolyEq", "solve_d2_polyeq_equation"],
    1.46          [("#Given" ,["equality e_e", "solveFor v_v"]),
    1.47            ("#Where" ,["(lhs e_e) is_poly_in v_v ", "((lhs e_e) has_degree_in v_v) = 2"]),
    1.48 @@ -1013,7 +1013,7 @@
    1.49    in
    1.50      Check_elementwise L_L {(v_v::real). Assumptions})"
    1.51  setup \<open>KEStore_Elems.add_mets
    1.52 -    [Method.prep_input thy "met_polyeq_d2_bdvonly" [] Method.id_empty
    1.53 +    [MethodC.prep_input thy "met_polyeq_d2_bdvonly" [] MethodC.id_empty
    1.54        (["PolyEq", "solve_d2_polyeq_bdvonly_equation"],
    1.55          [("#Given" ,["equality e_e", "solveFor v_v"]),
    1.56            ("#Where" ,["(lhs e_e) is_poly_in v_v ", "((lhs e_e) has_degree_in v_v) = 2"]),
    1.57 @@ -1036,7 +1036,7 @@
    1.58    in
    1.59      Check_elementwise L_L {(v_v::real). Assumptions})"
    1.60  setup \<open>KEStore_Elems.add_mets
    1.61 -    [Method.prep_input thy "met_polyeq_d2_sqonly" [] Method.id_empty
    1.62 +    [MethodC.prep_input thy "met_polyeq_d2_sqonly" [] MethodC.id_empty
    1.63        (["PolyEq", "solve_d2_polyeq_sqonly_equation"],
    1.64          [("#Given" ,["equality e_e", "solveFor v_v"]),
    1.65            ("#Where" ,["(lhs e_e) is_poly_in v_v ", "((lhs e_e) has_degree_in v_v) = 2"]),
    1.66 @@ -1059,7 +1059,7 @@
    1.67    in
    1.68      Check_elementwise L_L {(v_v::real). Assumptions})"
    1.69  setup \<open>KEStore_Elems.add_mets
    1.70 -    [Method.prep_input thy "met_polyeq_d2_pq" [] Method.id_empty
    1.71 +    [MethodC.prep_input thy "met_polyeq_d2_pq" [] MethodC.id_empty
    1.72        (["PolyEq", "solve_d2_polyeq_pq_equation"],
    1.73          [("#Given" ,["equality e_e", "solveFor v_v"]),
    1.74            ("#Where" ,["(lhs e_e) is_poly_in v_v ", "((lhs e_e) has_degree_in v_v) = 2"]),
    1.75 @@ -1081,7 +1081,7 @@
    1.76      L_L = Or_to_List e_e
    1.77    in Check_elementwise L_L {(v_v::real). Assumptions})"
    1.78  setup \<open>KEStore_Elems.add_mets
    1.79 -    [Method.prep_input thy "met_polyeq_d2_abc" [] Method.id_empty
    1.80 +    [MethodC.prep_input thy "met_polyeq_d2_abc" [] MethodC.id_empty
    1.81        (["PolyEq", "solve_d2_polyeq_abc_equation"],
    1.82          [("#Given" ,["equality e_e", "solveFor v_v"]),
    1.83            ("#Where" ,["(lhs e_e) is_poly_in v_v ", "((lhs e_e) has_degree_in v_v) = 2"]),
    1.84 @@ -1108,7 +1108,7 @@
    1.85    in
    1.86      Check_elementwise L_L {(v_v::real). Assumptions})"
    1.87  setup \<open>KEStore_Elems.add_mets
    1.88 -    [Method.prep_input thy "met_polyeq_d3" [] Method.id_empty
    1.89 +    [MethodC.prep_input thy "met_polyeq_d3" [] MethodC.id_empty
    1.90        (["PolyEq", "solve_d3_polyeq_equation"],
    1.91          [("#Given" ,["equality e_e", "solveFor v_v"]),
    1.92            ("#Where" ,["(lhs e_e) is_poly_in v_v ", "((lhs e_e) has_degree_in v_v) = 3"]),
    1.93 @@ -1138,7 +1138,7 @@
    1.94    in
    1.95      Or_to_List e_e)"
    1.96  setup \<open>KEStore_Elems.add_mets
    1.97 -    [Method.prep_input thy "met_polyeq_complsq" [] Method.id_empty
    1.98 +    [MethodC.prep_input thy "met_polyeq_complsq" [] MethodC.id_empty
    1.99        (["PolyEq", "complete_square"],
   1.100          [("#Given" ,["equality e_e", "solveFor v_v"]),
   1.101            ("#Where" ,["matches (?a = 0) e_e", "((lhs e_e) has_degree_in v_v) = 2"]),