1.1 --- a/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy	Wed Feb 03 15:21:12 2021 +0100
     1.2 +++ b/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy	Wed Feb 03 16:39:44 2021 +0100
     1.3 @@ -56,14 +56,14 @@
     1.4          Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)], NONE, 
     1.5          [["SignalProcessing", "Z_Transform", "Inverse"]]))]\<close>
     1.6  
     1.7 -subsection \<open>Setup Parent Nodes in Hierarchy of Method\<close>
     1.8 +subsection \<open>Setup Parent Nodes in Hierarchy of MethodC\<close>
     1.9  ML \<open>val thy = @{theory}; (*latest version of thy required*)\<close>
    1.10  setup \<open>KEStore_Elems.add_mets
    1.11 -    [Method.prep_input thy "met_SP" [] Method.id_empty
    1.12 +    [MethodC.prep_input thy "met_SP" [] MethodC.id_empty
    1.13        (["SignalProcessing"], [],
    1.14          {rew_ord'="tless_true", rls'= Rule_Set.empty, calc = [], srls = Rule_Set.empty, prls = Rule_Set.empty, crls = Rule_Set.empty,
    1.15            errpats = [], nrls = Rule_Set.empty}, @{thm refl}),
    1.16 -    Method.prep_input thy "met_SP_Ztrans" [] Method.id_empty
    1.17 +    MethodC.prep_input thy "met_SP_Ztrans" [] MethodC.id_empty
    1.18        (["SignalProcessing", "Z_Transform"], [],
    1.19          {rew_ord'="tless_true", rls'= Rule_Set.empty, calc = [], srls = Rule_Set.empty, prls = Rule_Set.empty, crls = Rule_Set.empty,
    1.20            errpats = [], nrls = Rule_Set.empty}, @{thm refl})]
    1.21 @@ -87,7 +87,7 @@
    1.22          [BOOL equ, REAL X_z]
    1.23    in X) "
    1.24  setup \<open>KEStore_Elems.add_mets
    1.25 -    [Method.prep_input thy "met_SP_Ztrans_inv" [] Method.id_empty
    1.26 +    [MethodC.prep_input thy "met_SP_Ztrans_inv" [] MethodC.id_empty
    1.27        (["SignalProcessing", "Z_Transform", "Inverse"],
    1.28          [("#Given" ,["filterExpression X_eq", "functionName X_z"]),
    1.29            ("#Find"  ,["stepResponse n_eq"])], \<comment> \<open>TODO: unused, "u [n]" is introduced by rule1..6\<close>
    1.30 @@ -115,7 +115,7 @@
    1.31      n_eq = (Rewrite_Set ''inverse_z'' ) X_zeq
    1.32    in n_eq)"
    1.33  setup \<open>KEStore_Elems.add_mets
    1.34 -    [Method.prep_input thy "met_SP_Ztrans_inv_sub" [] Method.id_empty
    1.35 +    [MethodC.prep_input thy "met_SP_Ztrans_inv_sub" [] MethodC.id_empty
    1.36        (["SignalProcessing", "Z_Transform", "Inverse_sub"],
    1.37          [("#Given" ,["filterExpression X_eq", "functionName X_z"]),
    1.38            ("#Find"  ,["stepResponse n_eq"])], \<comment> \<open>TODO: unused, "u [n]" is introduced by rule1..6\<close>