src/Tools/isac/Knowledge/Inverse_Z_Transform.thy
changeset 59997 46fe5a8c3911
parent 59973 8a46c2e7c27a
child 60154 2ab0d1523731
     1.1 --- a/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy	Tue May 19 12:33:35 2020 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy	Wed May 20 12:52:09 2020 +0200
     1.3 @@ -48,13 +48,13 @@
     1.4  setup \<open>KEStore_Elems.add_pbts
     1.5    [(Problem.prep_input thy "pbl_SP" [] Problem.id_empty (["SignalProcessing"], [], Rule_Set.empty, NONE, [])),
     1.6      (Problem.prep_input thy "pbl_SP_Ztrans" [] Problem.id_empty
     1.7 -      (["Z_Transform","SignalProcessing"], [], Rule_Set.empty, NONE, [])),
     1.8 +      (["Z_Transform", "SignalProcessing"], [], Rule_Set.empty, NONE, [])),
     1.9      (Problem.prep_input thy "pbl_SP_Ztrans_inv" [] Problem.id_empty
    1.10        (["Inverse", "Z_Transform", "SignalProcessing"],
    1.11          [("#Given" , ["filterExpression X_eq"]),
    1.12            ("#Find"  ,["stepResponse n_eq"])], \<comment> \<open>TODO: unused, "u [n]" is introduced by rule1..6\<close>
    1.13          Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)], NONE, 
    1.14 -        [["SignalProcessing","Z_Transform","Inverse"]]))]\<close>
    1.15 +        [["SignalProcessing", "Z_Transform", "Inverse"]]))]\<close>
    1.16  
    1.17  subsection \<open>Setup Parent Nodes in Hierarchy of Method\<close>
    1.18  ML \<open>val thy = @{theory}; (*latest version of thy required*)\<close>