test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy
changeset 60495 54642eaf7bba
parent 60469 89e1d8a633bb
child 60516 795d1352493a
     1.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy	Wed Jul 27 13:11:43 2022 +0200
     1.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy	Wed Jul 27 13:59:58 2022 +0200
     1.3 @@ -886,7 +886,7 @@
     1.4        with \em SignalProcessing \normalfont and go on by creating the node
     1.5        \em Z\_Transform\normalfont.\<close>
     1.6  
     1.7 -setup \<open>KEStore_Elems.add_pbts
     1.8 +setup \<open>KEStore_Elems.add_pbls
     1.9    [Problem.prep_input @{theory} "pbl_SP" [] Problem.id_empty (["SignalProcessing"], [], Rule_Set.empty, NONE, []),
    1.10      Problem.prep_input @{theory} "pbl_SP_Ztrans" [] Problem.id_empty
    1.11        (["Z_Transform", "SignalProcessing"], [], Rule_Set.empty, NONE, [])]\<close>
    1.12 @@ -895,7 +895,7 @@
    1.13         and output parameters. We already prepared their definition in
    1.14         Section~\ref{sec:deffdes}.\<close>
    1.15  
    1.16 -setup \<open>KEStore_Elems.add_pbts
    1.17 +setup \<open>KEStore_Elems.add_pbls
    1.18    [Problem.prep_input @{theory} "pbl_SP_Ztrans_inv" [] Problem.id_empty
    1.19        (["Inverse", "Z_Transform", "SignalProcessing"],
    1.20          [("#Given" ,["filterExpression X_eq"]),