1.1 --- a/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy Wed Nov 21 12:32:54 2018 +0100
1.2 +++ b/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy Wed Nov 28 11:46:00 2018 +0100
1.3 @@ -73,15 +73,17 @@
1.4 subsection \<open>Setup Parent Nodes in Hierarchy of Method\<close>
1.5 ML \<open>val thy = @{theory}; (*latest version of thy required*)\<close>
1.6 setup \<open>KEStore_Elems.add_mets
1.7 - [Specify.prep_met thy "met_SP" [] Celem.e_metID
1.8 + [Specify.prep_met thy "met_SP" [] Celem.e_metID
1.9 (["SignalProcessing"], [],
1.10 {rew_ord'="tless_true", rls'= Rule.e_rls, calc = [], srls = Rule.e_rls, prls = Rule.e_rls, crls = Rule.e_rls,
1.11 errpats = [], nrls = Rule.e_rls}, "empty_script"),
1.12 Specify.prep_met thy "met_SP_Ztrans" [] Celem.e_metID
1.13 (["SignalProcessing", "Z_Transform"], [],
1.14 {rew_ord'="tless_true", rls'= Rule.e_rls, calc = [], srls = Rule.e_rls, prls = Rule.e_rls, crls = Rule.e_rls,
1.15 - errpats = [], nrls = Rule.e_rls}, "empty_script"),
1.16 - Specify.prep_met thy "met_SP_Ztrans_inv" [] Celem.e_metID
1.17 + errpats = [], nrls = Rule.e_rls}, "empty_script")]
1.18 +\<close>
1.19 +setup \<open>KEStore_Elems.add_mets
1.20 + [Specify.prep_met thy "met_SP_Ztrans_inv" [] Celem.e_metID
1.21 (["SignalProcessing", "Z_Transform", "Inverse"],
1.22 [("#Given" ,["filterExpression (X_eq::bool)"]),
1.23 ("#Find" ,["stepResponse (n_eq::bool)"])],
1.24 @@ -101,8 +103,10 @@
1.25 " [LINEAR,univariate,equation,test]," ^
1.26 " [Test,solve_linear]) " ^
1.27 " [BOOL equ, REAL z]) " ^
1.28 - " in X)"),
1.29 - Specify.prep_met thy "met_SP_Ztrans_inv" [] Celem.e_metID
1.30 + " in X)")]
1.31 +\<close>
1.32 +setup \<open>KEStore_Elems.add_mets
1.33 + [Specify.prep_met thy "met_SP_Ztrans_inv" [] Celem.e_metID
1.34 (["SignalProcessing", "Z_Transform", "Inverse"],
1.35 [("#Given" ,["filterExpression X_eq"]),
1.36 ("#Find" ,["stepResponse n_eq"])],
1.37 @@ -174,8 +178,10 @@
1.38 " (X_z::bool) = Take (X_z = pbz); "^
1.39 " (n_eq::bool) = (Rewrite_Set inverse_z False) X_z; "^
1.40 " n_eq = drop_questionmarks n_eq "^
1.41 - "in n_eq)"),
1.42 - Specify.prep_met thy "met_SP_Ztrans_inv_sub" [] Celem.e_metID
1.43 + "in n_eq)")]
1.44 +\<close>
1.45 +setup \<open>KEStore_Elems.add_mets
1.46 + [Specify.prep_met thy "met_SP_Ztrans_inv_sub" [] Celem.e_metID
1.47 (["SignalProcessing", "Z_Transform", "Inverse_sub"],
1.48 [("#Given" ,["filterExpression X_eq"]),
1.49 ("#Find" ,["stepResponse n_eq"])],