1.1 --- a/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy	Sun Jun 20 12:45:03 2021 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy	Sun Jun 20 16:26:18 2021 +0200
     1.3 @@ -43,16 +43,16 @@
     1.4  
     1.5  subsection\<open>Define the Specification\<close>
     1.6  
     1.7 -setup \<open>KEStore_Elems.add_pbts
     1.8 -  [(Problem.prep_input @{theory} "pbl_SP" [] Problem.id_empty (["SignalProcessing"], [], Rule_Set.empty, NONE, [])),
     1.9 -    (Problem.prep_input @{theory} "pbl_SP_Ztrans" [] Problem.id_empty
    1.10 -      (["Z_Transform", "SignalProcessing"], [], Rule_Set.empty, NONE, [])),
    1.11 -    (Problem.prep_input @{theory} "pbl_SP_Ztrans_inv" [] Problem.id_empty
    1.12 -      (["Inverse", "Z_Transform", "SignalProcessing"],
    1.13 -        [("#Given" , ["filterExpression X_eq"]),
    1.14 -          ("#Find"  ,["stepResponse n_eq"])], \<comment> \<open>TODO: unused, "u [n]" is introduced by rule1..6\<close>
    1.15 -        Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)], NONE, 
    1.16 -        [["SignalProcessing", "Z_Transform", "Inverse"]]))]\<close>
    1.17 +problem pbl_SP : "SignalProcessing" = \<open>Rule_Set.empty\<close>
    1.18 +
    1.19 +problem pbl_SP_Ztrans : "Z_Transform/SignalProcessing" = \<open>Rule_Set.empty\<close>
    1.20 +
    1.21 +problem pbl_SP_Ztrans_inv : "Inverse/Z_Transform/SignalProcessing" =
    1.22 +  \<open>Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)]\<close>
    1.23 +  Method: "SignalProcessing/Z_Transform/Inverse"
    1.24 +  Given: "filterExpression X_eq"
    1.25 +  Find: "stepResponse n_eq" \<comment> \<open>TODO: unused, "u [n]" is introduced by rule1..6\<close>
    1.26 +
    1.27  
    1.28  subsection \<open>Setup Parent Nodes in Hierarchy of MethodC\<close>
    1.29