src/Tools/isac/Knowledge/Inverse_Z_Transform.thy
changeset 59505 a1f223658994
parent 59504 546bd1b027cc
child 59512 e504168e7b01
     1.1 --- a/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy	Tue Feb 19 19:35:12 2019 +0100
     1.2 +++ b/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy	Thu Feb 28 12:14:32 2019 +0100
     1.3 @@ -82,6 +82,7 @@
     1.4          {rew_ord'="tless_true", rls'= Rule.e_rls, calc = [], srls = Rule.e_rls, prls = Rule.e_rls, crls = Rule.e_rls,
     1.5            errpats = [], nrls = Rule.e_rls}, "empty_script")]
     1.6  \<close>
     1.7 +(*ok
     1.8  partial_function (tailrec) inverse_ztransform :: "bool \<Rightarrow> bool"
     1.9    where
    1.10  "inverse_ztransform X_eq =                                           \<comment> \<open>(1/z) instead of z ^^^ -1\<close>                
    1.11 @@ -96,6 +97,7 @@
    1.12        L_L = SubProblem (''Test'', [''LINEAR'',''univariate'',''equation'',''test''],         
    1.13                  [''Test'',''solve_linear'']) [BOOL equ, STRING ''z'']              \<comment> \<open>PROG string\<close>
    1.14    in X) "
    1.15 +*)
    1.16  setup \<open>KEStore_Elems.add_mets
    1.17      [Specify.prep_met thy "met_SP_Ztrans_inv" [] Celem.e_metID
    1.18        (["SignalProcessing", "Z_Transform", "Inverse"],