1.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy	Sat Jun 01 11:09:19 2019 +0200
     1.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy	Sat Jun 22 13:15:52 2019 +0200
     1.3 @@ -894,7 +894,7 @@
     1.4  setup \<open>KEStore_Elems.add_pbts
     1.5    [prep_pbt thy "pbl_SP_Ztrans_inv" [] e_pblID
     1.6        (["Inverse", "Z_Transform", "SignalProcessing"],
     1.7 -        [("#Given", ["filterExpression X_eq"]),
     1.8 +        [("#Given" ,["filterExpression X_eq"]),
     1.9            ("#Find", ["stepResponse n_eq"])],
    1.10          append_rls "e_rls" e_rls [(*for preds in where_*)],
    1.11          NONE,
    1.12 @@ -940,7 +940,8 @@
    1.13  setup \<open>KEStore_Elems.add_mets
    1.14    [prep_met thy "met_SP_Ztrans_inv" [] e_metID
    1.15        (["SignalProcessing", "Z_Transform", "Inverse"], 
    1.16 -        [("#Given" ,["filterExpression X_eq"]), ("#Find"  ,["stepResponse n_eq"])],
    1.17 +        [("#Given" ,["filterExpression X_eq", "boundVariable X_z"]),
    1.18 +          ("#Find", ["stepResponse n_eq"])],
    1.19          {rew_ord'="tless_true", rls'= e_rls, calc = [], srls = e_rls, prls = e_rls, crls = e_rls,
    1.20            errpats = [], nrls = e_rls},
    1.21          "empty_script")]
    1.22 @@ -953,10 +954,11 @@
    1.23  setup \<open>KEStore_Elems.add_mets
    1.24    [prep_met thy "met_SP_Ztrans_inv" [] e_metID
    1.25        (["SignalProcessing", "Z_Transform", "Inverse"], 
    1.26 -        [("#Given" ,["filterExpression X_eq"]), ("#Find"  ,["stepResponse n_eq"])],
    1.27 +        [("#Given" , ["filterExpression X_eq", "boundVariable X_z"]),
    1.28 +          ("#Find", ["stepResponse n_eq"])],
    1.29          {rew_ord'="tless_true", rls'= e_rls, calc = [], srls = e_rls, prls = e_rls, crls = e_rls,
    1.30            errpats = [], nrls = e_rls},
    1.31 -        "Script InverseZTransform (Xeq::bool) =" ^
    1.32 +        "Script InverseZTransform (Xeq::bool) =" ^ (*TODO boundVariable X_z*)
    1.33            " (let X = Take Xeq;" ^
    1.34            "      X = Rewrite ruleZY False X" ^
    1.35            "  in X)")]
    1.36 @@ -1127,7 +1129,8 @@
    1.37  setup \<open>KEStore_Elems.add_mets
    1.38    [prep_met thy "met_SP_Ztrans_inv" [] e_metID
    1.39        (["SignalProcessing", "Z_Transform", "Inverse"], 
    1.40 -        [("#Given" ,["filterExpression X_eq"]), ("#Find"  ,["stepResponse n_eq"])],
    1.41 +        [("#Given" , ["filterExpression X_eq"]), (*TODO boundVariable X_z*)
    1.42 +          ("#Find", ["stepResponse n_eq"])],
    1.43          {rew_ord'="tless_true", rls'= e_rls, calc = [], srls = srls, prls = e_rls, crls = e_rls,
    1.44            errpats = [], nrls = e_rls},
    1.45          "Script InverseZTransform (X_eq::bool) =                        "^