1.1 --- a/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy	Wed Apr 22 11:23:30 2020 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy	Wed Apr 22 14:36:27 2020 +0200
     1.3 @@ -46,10 +46,10 @@
     1.4  val thy = @{theory};
     1.5  \<close>
     1.6  setup \<open>KEStore_Elems.add_pbts
     1.7 -  [(Specify.prep_pbt thy "pbl_SP" [] Spec.e_pblID (["SignalProcessing"], [], Rule_Set.empty, NONE, [])),
     1.8 -    (Specify.prep_pbt thy "pbl_SP_Ztrans" [] Spec.e_pblID
     1.9 +  [(Specify.prep_pbt thy "pbl_SP" [] Problem.id_empty (["SignalProcessing"], [], Rule_Set.empty, NONE, [])),
    1.10 +    (Specify.prep_pbt thy "pbl_SP_Ztrans" [] Problem.id_empty
    1.11        (["Z_Transform","SignalProcessing"], [], Rule_Set.empty, NONE, [])),
    1.12 -    (Specify.prep_pbt thy "pbl_SP_Ztrans_inv" [] Spec.e_pblID
    1.13 +    (Specify.prep_pbt thy "pbl_SP_Ztrans_inv" [] Problem.id_empty
    1.14        (["Inverse", "Z_Transform", "SignalProcessing"],
    1.15          [("#Given" , ["filterExpression X_eq"]),
    1.16            ("#Find"  ,["stepResponse n_eq"])], \<comment> \<open>TODO: unused, "u [n]" is introduced by rule1..6\<close>
    1.17 @@ -59,11 +59,11 @@
    1.18  subsection \<open>Setup Parent Nodes in Hierarchy of Method\<close>
    1.19  ML \<open>val thy = @{theory}; (*latest version of thy required*)\<close>
    1.20  setup \<open>KEStore_Elems.add_mets
    1.21 -    [Specify.prep_met thy "met_SP" [] Spec.e_metID
    1.22 +    [Specify.prep_met thy "met_SP" [] Method.id_empty
    1.23        (["SignalProcessing"], [],
    1.24          {rew_ord'="tless_true", rls'= Rule_Set.empty, calc = [], srls = Rule_Set.empty, prls = Rule_Set.empty, crls = Rule_Set.empty,
    1.25            errpats = [], nrls = Rule_Set.empty}, @{thm refl}),
    1.26 -    Specify.prep_met thy "met_SP_Ztrans" [] Spec.e_metID
    1.27 +    Specify.prep_met thy "met_SP_Ztrans" [] Method.id_empty
    1.28        (["SignalProcessing", "Z_Transform"], [],
    1.29          {rew_ord'="tless_true", rls'= Rule_Set.empty, calc = [], srls = Rule_Set.empty, prls = Rule_Set.empty, crls = Rule_Set.empty,
    1.30            errpats = [], nrls = Rule_Set.empty}, @{thm refl})]
    1.31 @@ -87,7 +87,7 @@
    1.32          [BOOL equ, REAL X_z]
    1.33    in X) "
    1.34  setup \<open>KEStore_Elems.add_mets
    1.35 -    [Specify.prep_met thy "met_SP_Ztrans_inv" [] Spec.e_metID
    1.36 +    [Specify.prep_met thy "met_SP_Ztrans_inv" [] Method.id_empty
    1.37        (["SignalProcessing", "Z_Transform", "Inverse"],
    1.38          [("#Given" ,["filterExpression X_eq", "functionName X_z"]),
    1.39            ("#Find"  ,["stepResponse n_eq"])], \<comment> \<open>TODO: unused, "u [n]" is introduced by rule1..6\<close>
    1.40 @@ -115,7 +115,7 @@
    1.41      n_eq = (Rewrite_Set ''inverse_z'' ) X_zeq
    1.42    in n_eq)"
    1.43  setup \<open>KEStore_Elems.add_mets
    1.44 -    [Specify.prep_met thy "met_SP_Ztrans_inv_sub" [] Spec.e_metID
    1.45 +    [Specify.prep_met thy "met_SP_Ztrans_inv_sub" [] Method.id_empty
    1.46        (["SignalProcessing", "Z_Transform", "Inverse_sub"],
    1.47          [("#Given" ,["filterExpression X_eq", "functionName X_z"]),
    1.48            ("#Find"  ,["stepResponse n_eq"])], \<comment> \<open>TODO: unused, "u [n]" is introduced by rule1..6\<close>