1.1 --- a/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy	Mon Jan 20 16:15:34 2014 +0100
     1.2 +++ b/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy	Tue Jan 21 00:27:44 2014 +0100
     1.3 @@ -73,6 +73,24 @@
     1.4      append_rls "e_rls" e_rls [(*for preds in where_*)], NONE, 
     1.5      [["SignalProcessing","Z_Transform","Inverse"]]));
     1.6  *}
     1.7 +setup {* KEStore_Elems.store_pbts
     1.8 +  [(prep_pbt thy "pbl_SP" [] e_pblID (["SignalProcessing"], [], e_rls, NONE, [])),
     1.9 +    (prep_pbt thy "pbl_SP_Ztrans" [] e_pblID
    1.10 +      (["Z_Transform","SignalProcessing"], [], e_rls, NONE, [])),
    1.11 +    (prep_pbt thy "pbl_SP_Ztrans_inv" [] e_pblID
    1.12 +      (["Inverse", "Z_Transform", "SignalProcessing"],
    1.13 +        (*^ capital letter breaks coding standard
    1.14 +          because "inverse" = Const ("Rings.inverse_class.inverse", ..*)
    1.15 +        [("#Given" ,["filterExpression (X_eq::bool)"]),
    1.16 +          ("#Find"  ,["stepResponse (n_eq::bool)"])],
    1.17 +        append_rls "e_rls" e_rls [(*for preds in where_*)], NONE, 
    1.18 +        [["SignalProcessing","Z_Transform","Inverse"]])),
    1.19 +    (prep_pbt thy "pbl_SP_Ztrans_inv" [] e_pblID
    1.20 +      (["Inverse", "Z_Transform", "SignalProcessing"],
    1.21 +        [("#Given" ,["filterExpression X_eq"]),
    1.22 +          ("#Find"  ,["stepResponse n_eq"])],
    1.23 +        append_rls "e_rls" e_rls [(*for preds in where_*)], NONE, 
    1.24 +        [["SignalProcessing","Z_Transform","Inverse"]]))] *}
    1.25  
    1.26  subsection {*Define Name and Signature for the Method*}
    1.27  consts