1.1 --- a/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy	Wed Dec 14 14:20:25 2016 +0100
     1.2 +++ b/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy	Sun Dec 18 16:27:41 2016 +0100
     1.3 @@ -47,10 +47,10 @@
     1.4  val thy = @{theory};
     1.5  *}
     1.6  setup {* KEStore_Elems.add_pbts
     1.7 -  [(prep_pbt thy "pbl_SP" [] e_pblID (["SignalProcessing"], [], e_rls, NONE, [])),
     1.8 -    (prep_pbt thy "pbl_SP_Ztrans" [] e_pblID
     1.9 +  [(Specify.prep_pbt thy "pbl_SP" [] e_pblID (["SignalProcessing"], [], e_rls, NONE, [])),
    1.10 +    (Specify.prep_pbt thy "pbl_SP_Ztrans" [] e_pblID
    1.11        (["Z_Transform","SignalProcessing"], [], e_rls, NONE, [])),
    1.12 -    (prep_pbt thy "pbl_SP_Ztrans_inv" [] e_pblID
    1.13 +    (Specify.prep_pbt thy "pbl_SP_Ztrans_inv" [] e_pblID
    1.14        (["Inverse", "Z_Transform", "SignalProcessing"],
    1.15          (*^ capital letter breaks coding standard
    1.16            because "inverse" = Const ("Rings.inverse_class.inverse", ..*)
    1.17 @@ -58,7 +58,7 @@
    1.18            ("#Find"  ,["stepResponse (n_eq::bool)"])],
    1.19          append_rls "e_rls" e_rls [(*for preds in where_*)], NONE, 
    1.20          [["SignalProcessing","Z_Transform","Inverse"]])),
    1.21 -    (prep_pbt thy "pbl_SP_Ztrans_inv" [] e_pblID
    1.22 +    (Specify.prep_pbt thy "pbl_SP_Ztrans_inv" [] e_pblID
    1.23        (["Inverse", "Z_Transform", "SignalProcessing"],
    1.24          [("#Given" ,["filterExpression X_eq"]),
    1.25            ("#Find"  ,["stepResponse n_eq"])],
    1.26 @@ -73,15 +73,15 @@
    1.27  subsection {*Setup Parent Nodes in Hierarchy of Method*}
    1.28  ML {* val thy = @{theory}; (*latest version of thy required*) *}
    1.29  setup {* KEStore_Elems.add_mets
    1.30 -  [prep_met thy "met_SP" [] e_metID
    1.31 +  [Specify.prep_met thy "met_SP" [] e_metID
    1.32        (["SignalProcessing"], [],
    1.33          {rew_ord'="tless_true", rls'= e_rls, calc = [], srls = e_rls, prls = e_rls, crls = e_rls,
    1.34            errpats = [], nrls = e_rls}, "empty_script"),
    1.35 -    prep_met thy "met_SP_Ztrans" [] e_metID
    1.36 +    Specify.prep_met thy "met_SP_Ztrans" [] e_metID
    1.37        (["SignalProcessing", "Z_Transform"], [],
    1.38          {rew_ord'="tless_true", rls'= e_rls, calc = [], srls = e_rls, prls = e_rls, crls = e_rls,
    1.39            errpats = [], nrls = e_rls}, "empty_script"),
    1.40 -    prep_met thy "met_SP_Ztrans_inv" [] e_metID
    1.41 +    Specify.prep_met thy "met_SP_Ztrans_inv" [] e_metID
    1.42        (["SignalProcessing", "Z_Transform", "Inverse"], 
    1.43          [("#Given" ,["filterExpression (X_eq::bool)"]),
    1.44            ("#Find"  ,["stepResponse (n_eq::bool)"])],
    1.45 @@ -102,7 +102,7 @@
    1.46            "                         [Test,solve_linear])              " ^
    1.47            "                        [BOOL equ, REAL z])              " ^
    1.48            "  in X)"),
    1.49 -    prep_met thy "met_SP_Ztrans_inv" [] e_metID
    1.50 +    Specify.prep_met thy "met_SP_Ztrans_inv" [] e_metID
    1.51        (["SignalProcessing", "Z_Transform", "Inverse"], 
    1.52          [("#Given" ,["filterExpression X_eq"]),
    1.53            ("#Find"  ,["stepResponse n_eq"])],
    1.54 @@ -175,7 +175,7 @@
    1.55             "      (n_eq::bool) = (Rewrite_Set inverse_z False) X_z;        "^
    1.56             "      n_eq = drop_questionmarks n_eq                           "^
    1.57             "in n_eq)"),
    1.58 -    prep_met thy "met_SP_Ztrans_inv_sub" [] e_metID
    1.59 +    Specify.prep_met thy "met_SP_Ztrans_inv_sub" [] e_metID
    1.60        (["SignalProcessing", "Z_Transform", "Inverse_sub"], 
    1.61          [("#Given" ,["filterExpression X_eq"]),
    1.62            ("#Find"  ,["stepResponse n_eq"])],