test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy
changeset 60290 bb4e8b01b072
parent 60278 343efa173023
child 60297 73e7175a7d3f
     1.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy	Thu Jun 10 11:54:20 2021 +0200
     1.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy	Thu Jun 10 12:23:57 2021 +0200
     1.3 @@ -885,8 +885,8 @@
     1.4        \em Z\_Transform\normalfont.\<close>
     1.5  
     1.6  setup \<open>KEStore_Elems.add_pbts
     1.7 -  [Problem.prep_input thy "pbl_SP" [] Problem.id_empty (["SignalProcessing"], [], Rule_Set.empty, NONE, []),
     1.8 -    Problem.prep_input thy "pbl_SP_Ztrans" [] Problem.id_empty
     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  
    1.13  text\<open>\noindent For the suddenly created node we have to define the input
    1.14 @@ -894,7 +894,7 @@
    1.15         Section~\ref{sec:deffdes}.\<close>
    1.16  
    1.17  setup \<open>KEStore_Elems.add_pbts
    1.18 -  [Problem.prep_input thy "pbl_SP_Ztrans_inv" [] Problem.id_empty
    1.19 +  [Problem.prep_input @{theory} "pbl_SP_Ztrans_inv" [] Problem.id_empty
    1.20        (["Inverse", "Z_Transform", "SignalProcessing"],
    1.21          [("#Given" ,["filterExpression X_eq"]),
    1.22            ("#Find", ["stepResponse n_eq"])],
    1.23 @@ -923,12 +923,12 @@
    1.24        as content.\<close>
    1.25  
    1.26  setup \<open>KEStore_Elems.add_mets
    1.27 -  [MethodC.prep_input thy "met_SP" [] e_metID
    1.28 +  [MethodC.prep_input @{theory} "met_SP" [] e_metID
    1.29        (["SignalProcessing"], [],
    1.30          {rew_ord'="tless_true", rls'= Rule_Set.empty, calc = [], srls = Rule_Set.empty, prls = Rule_Set.empty, crls = Rule_Set.empty,
    1.31            errpats = [], nrls = Rule_Set.empty},
    1.32          "empty_script"),
    1.33 -    MethodC.prep_input thy "met_SP_Ztrans" [] e_metID
    1.34 +    MethodC.prep_input @{theory} "met_SP_Ztrans" [] e_metID
    1.35        (["SignalProcessing", "Z_Transform"], [],
    1.36          {rew_ord'="tless_true", rls'= Rule_Set.empty, calc = [], srls = Rule_Set.empty, prls = Rule_Set.empty, crls = Rule_Set.empty,
    1.37            errpats = [], nrls = Rule_Set.empty},