1.1 --- a/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy	Mon Nov 07 17:37:20 2022 +0100
     1.2 +++ b/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy	Mon Nov 07 19:49:14 2022 +0100
     1.3 @@ -57,11 +57,11 @@
     1.4  subsection \<open>Setup Parent Nodes in Hierarchy of MethodC\<close>
     1.5  
     1.6  method met_SP : "SignalProcessing" =
     1.7 -  \<open>{rew_ord="tless_true", rls'= Rule_Set.empty, calc = [], prog_rls = Rule_Set.empty, where_rls = Rule_Set.empty, crls = Rule_Set.empty,
     1.8 +  \<open>{rew_ord="tless_true", rls'= Rule_Set.empty, calc = [], prog_rls = Rule_Set.empty, where_rls = Rule_Set.empty,
     1.9      errpats = [], rew_rls = Rule_Set.empty}\<close>
    1.10  
    1.11  method met_SP_Ztrans : "SignalProcessing/Z_Transform" =
    1.12 -  \<open>{rew_ord="tless_true", rls'= Rule_Set.empty, calc = [], prog_rls = Rule_Set.empty, where_rls = Rule_Set.empty, crls = Rule_Set.empty,
    1.13 +  \<open>{rew_ord="tless_true", rls'= Rule_Set.empty, calc = [], prog_rls = Rule_Set.empty, where_rls = Rule_Set.empty,
    1.14      errpats = [], rew_rls = Rule_Set.empty}\<close>
    1.15  
    1.16  partial_function (tailrec) inverse_ztransform :: "bool \<Rightarrow> real \<Rightarrow> bool"
    1.17 @@ -83,7 +83,7 @@
    1.18    in X) "
    1.19  
    1.20  method met_SP_Ztrans_inv : "SignalProcessing/Z_Transform/Inverse" =
    1.21 -  \<open>{rew_ord="tless_true", rls'= Rule_Set.empty, calc = [], prog_rls = Rule_Set.empty, where_rls = Rule_Set.empty, crls = Rule_Set.empty,
    1.22 +  \<open>{rew_ord="tless_true", rls'= Rule_Set.empty, calc = [], prog_rls = Rule_Set.empty, where_rls = Rule_Set.empty,
    1.23      errpats = [], rew_rls = Rule_Set.empty}\<close>
    1.24    Program: inverse_ztransform.simps
    1.25    Given: "filterExpression X_eq" "functionName X_z"
    1.26 @@ -127,7 +127,7 @@
    1.27          \<^rule_eval>\<open>get_numerator\<close> (eval_get_numerator "#get_numerator"),
    1.28          \<^rule_eval>\<open>factors_from_solution\<close> (eval_factors_from_solution "#factors_from_solution")],
    1.29        program = Rule.Empty_Prog},
    1.30 -    where_rls = Rule_Set.empty, crls = Rule_Set.empty, errpats = [], rew_rls = norm_Rational}\<close>
    1.31 +    where_rls = Rule_Set.empty, errpats = [], rew_rls = norm_Rational}\<close>
    1.32    Program: inverse_ztransform2.simps
    1.33    Given: "filterExpression X_eq" "functionName X_z"
    1.34    Find: "stepResponse n_eq" \<comment> \<open>TODO: unused, "u [n]" is introduced by rule1..6\<close>