1.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy	Wed Feb 03 15:21:12 2021 +0100
     1.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy	Wed Feb 03 16:39:44 2021 +0100
     1.3 @@ -513,12 +513,12 @@
     1.4  section \<open>Methods\<close>
     1.5  
     1.6  setup \<open>KEStore_Elems.add_mets
     1.7 -    [Method.prep_input thy "met_eqsys" [] Method.id_empty
     1.8 +    [MethodC.prep_input thy "met_eqsys" [] MethodC.id_empty
     1.9  	    (["EqSystem"], [],
    1.10  	      {rew_ord'="tless_true", rls' = Rule_Set.Empty, calc = [], srls = Rule_Set.Empty, prls = Rule_Set.Empty, crls = Rule_Set.Empty,
    1.11            errpats = [], nrls = Rule_Set.Empty},
    1.12  	      @{thm refl}),
    1.13 -    Method.prep_input thy "met_eqsys_topdown" [] Method.id_empty
    1.14 +    MethodC.prep_input thy "met_eqsys_topdown" [] MethodC.id_empty
    1.15        (["EqSystem", "top_down_substitution"], [],
    1.16          {rew_ord'="tless_true", rls' = Rule_Set.Empty, calc = [], srls = Rule_Set.Empty, prls = Rule_Set.Empty, crls = Rule_Set.Empty,
    1.17            errpats = [], nrls = Rule_Set.Empty},
    1.18 @@ -545,7 +545,7 @@
    1.19    in
    1.20      Try (Rewrite_Set ''order_system'' ) e__s)                              "
    1.21  setup \<open>KEStore_Elems.add_mets
    1.22 -    [Method.prep_input thy "met_eqsys_topdown_2x2" [] Method.id_empty
    1.23 +    [MethodC.prep_input thy "met_eqsys_topdown_2x2" [] MethodC.id_empty
    1.24        (["EqSystem", "top_down_substitution", "2x2"],
    1.25          [("#Given", ["equalities e_s", "solveForVars v_s"]),
    1.26            ("#Where",
    1.27 @@ -561,7 +561,7 @@
    1.28  	      @{thm solve_system.simps})]
    1.29  \<close>
    1.30  setup \<open>KEStore_Elems.add_mets
    1.31 -    [Method.prep_input thy "met_eqsys_norm" [] Method.id_empty
    1.32 +    [MethodC.prep_input thy "met_eqsys_norm" [] MethodC.id_empty
    1.33  	    (["EqSystem", "normalise"], [],
    1.34  	      {rew_ord'="tless_true", rls' = Rule_Set.Empty, calc = [], srls = Rule_Set.Empty, prls = Rule_Set.Empty, crls = Rule_Set.Empty,
    1.35            errpats = [], nrls = Rule_Set.Empty},
    1.36 @@ -583,7 +583,7 @@
    1.37      SubProblem (''EqSystem'', [''LINEAR'', ''system''], [''no_met''])
    1.38        [BOOL_LIST e__s, REAL_LIST v_s])"
    1.39  setup \<open>KEStore_Elems.add_mets
    1.40 -    [Method.prep_input thy "met_eqsys_norm_2x2" [] Method.id_empty
    1.41 +    [MethodC.prep_input thy "met_eqsys_norm_2x2" [] MethodC.id_empty
    1.42  	    (["EqSystem", "normalise", "2x2"],
    1.43  	      [("#Given" ,["equalities e_s", "solveForVars v_s"]),
    1.44  		      ("#Find"  ,["solution ss'''"])],
    1.45 @@ -615,7 +615,7 @@
    1.46      SubProblem (''EqSystem'', [''LINEAR'', ''system''], [''no_met''])
    1.47        [BOOL_LIST e__s, REAL_LIST v_s])"
    1.48  setup \<open>KEStore_Elems.add_mets
    1.49 -    [Method.prep_input thy "met_eqsys_norm_4x4" [] Method.id_empty
    1.50 +    [MethodC.prep_input thy "met_eqsys_norm_4x4" [] MethodC.id_empty
    1.51  	      (["EqSystem", "normalise", "4x4"],
    1.52  	       [("#Given" ,["equalities e_s", "solveForVars v_s"]),
    1.53  	         ("#Find"  ,["solution ss'''"])],
    1.54 @@ -647,7 +647,7 @@
    1.55    in
    1.56      [e_1, e_2, NTH 3 e_s, NTH 4 e_s])"
    1.57  setup \<open>KEStore_Elems.add_mets
    1.58 -    [Method.prep_input thy "met_eqsys_topdown_4x4" [] Method.id_empty
    1.59 +    [MethodC.prep_input thy "met_eqsys_topdown_4x4" [] MethodC.id_empty
    1.60  	    (["EqSystem", "top_down_substitution", "4x4"],
    1.61  	      [("#Given" ,["equalities e_s", "solveForVars v_s"]),
    1.62  	        ("#Where" , (*accepts missing variables up to diagonal form*)