test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy
changeset 59973 8a46c2e7c27a
parent 59971 2909d58a5c5d
child 59977 e635534c5f63
     1.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy	Wed May 13 12:14:49 2020 +0200
     1.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy	Wed May 13 16:10:22 2020 +0200
     1.3 @@ -883,8 +883,8 @@
     1.4        \em Z\_Transform\normalfont.\<close>
     1.5  
     1.6  setup \<open>KEStore_Elems.add_pbts
     1.7 -  [prep_pbt thy "pbl_SP" [] Problem.id_empty (["SignalProcessing"], [], Rule_Set.empty, NONE, []),
     1.8 -    prep_pbt thy "pbl_SP_Ztrans" [] Problem.id_empty
     1.9 +  [Problem.prep_input thy "pbl_SP" [] Problem.id_empty (["SignalProcessing"], [], Rule_Set.empty, NONE, []),
    1.10 +    Problem.prep_input thy "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 @@ -892,7 +892,7 @@
    1.15         Section~\ref{sec:deffdes}.\<close>
    1.16  
    1.17  setup \<open>KEStore_Elems.add_pbts
    1.18 -  [prep_pbt thy "pbl_SP_Ztrans_inv" [] Problem.id_empty
    1.19 +  [Problem.prep_input thy "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 @@ -921,12 +921,12 @@
    1.24        as content.\<close>
    1.25  
    1.26  setup \<open>KEStore_Elems.add_mets
    1.27 -  [prep_met thy "met_SP" [] e_metID
    1.28 +  [Method.prep_input thy "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 -    prep_met thy "met_SP_Ztrans" [] e_metID
    1.34 +    Method.prep_input thy "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},
    1.38 @@ -938,7 +938,7 @@
    1.39        of the script in e.g. the in- and output.\<close>
    1.40  
    1.41  setup \<open>KEStore_Elems.add_mets
    1.42 -  [prep_met thy "met_SP_Ztrans_inv" [] e_metID
    1.43 +  [Method.prep_input thy "met_SP_Ztrans_inv" [] e_metID
    1.44        (["SignalProcessing", "Z_Transform", "Inverse"], 
    1.45          [("#Given" ,["filterExpression X_eq", "boundVariable X_z"]),
    1.46            ("#Find", ["stepResponse n_eq"])],
    1.47 @@ -952,7 +952,7 @@
    1.48        simple operation.\<close>
    1.49  
    1.50  setup \<open>KEStore_Elems.add_mets
    1.51 -  [prep_met thy "met_SP_Ztrans_inv" [] e_metID
    1.52 +  [Method.prep_input thy "met_SP_Ztrans_inv" [] e_metID
    1.53        (["SignalProcessing", "Z_Transform", "Inverse"], 
    1.54          [("#Given" , ["filterExpression X_eq", "boundVariable X_z"]),
    1.55            ("#Find", ["stepResponse n_eq"])],
    1.56 @@ -1122,7 +1122,7 @@
    1.57        subversion.\<close>
    1.58  
    1.59  setup \<open>KEStore_Elems.add_mets
    1.60 -  [prep_met thy "met_SP_Ztrans_inv" [] e_metID
    1.61 +  [Method.prep_input thy "met_SP_Ztrans_inv" [] e_metID
    1.62        (["SignalProcessing", "Z_Transform", "Inverse"], 
    1.63          [("#Given" , ["filterExpression X_eq"]), (*TODO boundVariable X_z*)
    1.64            ("#Find", ["stepResponse n_eq"])],