1.1 --- a/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy	Mon Jan 27 21:58:57 2014 +0100
     1.2 +++ b/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy	Mon Jan 27 22:26:51 2014 +0100
     1.3 @@ -45,33 +45,6 @@
     1.4  subsection{*Define the Specification*}
     1.5  ML {*
     1.6  val thy = @{theory};
     1.7 -
     1.8 -store_pbt
     1.9 - (prep_pbt thy "pbl_SP" [] e_pblID
    1.10 - (["SignalProcessing"], [], e_rls, NONE, []));
    1.11 -store_pbt
    1.12 - (prep_pbt thy "pbl_SP_Ztrans" [] e_pblID
    1.13 - (["Z_Transform","SignalProcessing"], [], e_rls, NONE, []));
    1.14 -store_pbt
    1.15 - (prep_pbt thy "pbl_SP_Ztrans_inv" [] e_pblID
    1.16 - (["Inverse", "Z_Transform", "SignalProcessing"],
    1.17 -  (*^ capital letter breaks coding standard
    1.18 -    because "inverse" = Const ("Rings.inverse_class.inverse", ..*)
    1.19 -  [("#Given" ,["filterExpression (X_eq::bool)"]),
    1.20 -   ("#Find"  ,["stepResponse (n_eq::bool)"])
    1.21 -  ],
    1.22 -  append_rls "e_rls" e_rls [(*for preds in where_*)], NONE, 
    1.23 -  [["SignalProcessing","Z_Transform","Inverse"]]));
    1.24 -*}
    1.25 -ML {*
    1.26 -  store_pbt
    1.27 -   (prep_pbt thy "pbl_SP_Ztrans_inv" [] e_pblID
    1.28 -   (["Inverse", "Z_Transform", "SignalProcessing"],
    1.29 -    [("#Given" ,["filterExpression X_eq"]),
    1.30 -     ("#Find"  ,["stepResponse n_eq"])
    1.31 -    ],
    1.32 -    append_rls "e_rls" e_rls [(*for preds in where_*)], NONE, 
    1.33 -    [["SignalProcessing","Z_Transform","Inverse"]]));
    1.34  *}
    1.35  setup {* KEStore_Elems.add_pbts
    1.36    [(prep_pbt thy "pbl_SP" [] e_pblID (["SignalProcessing"], [], e_rls, NONE, [])),