1.1 --- a/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy	Mon Apr 08 16:10:07 2019 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy	Tue Apr 09 11:38:26 2019 +0200
     1.3 @@ -17,8 +17,10 @@
     1.4    rule42: "(a * (z/(z-b)) + c * (z/(z-d))) = (a * b^^^n * u [n] + c * d^^^n * u [n])"*)
     1.5  
     1.6  axiomatization where
     1.7 +(*ruleZY: "(X z = a / b) = (d_d z X = a / (z * b))"         ..looks better, but types are flawed*)
     1.8    ruleZY: "(X z = a / b) = (X' z = a / (z * b))" and
     1.9 -  ruleYZ: "(a/b + c/d) = (a*(z/b) + c*(z/d))" 
    1.10 +  ruleYZ: "a / (z - b) + c / (z - d) = a * (z / (z - b)) + c * (z / (z - d))" and
    1.11 +  ruleYZa: "(a / b + c / d) = (a * (z / b) + c * (z / d))"        \<comment> \<open>that is what students learn\<close>
    1.12  
    1.13  subsection\<open>Define the Field Descriptions for the specification\<close>
    1.14  consts
    1.15 @@ -95,7 +97,7 @@
    1.16        fun_arg = Take (lhs X');                                                      
    1.17        arg = (Rewrite_Set ''partial_fraction'' False) X';                     \<comment> \<open>get_argument TODO\<close>      
    1.18        L_L = SubProblem (''Test'', [''LINEAR'',''univariate'',''equation'',''test''],         
    1.19 -                [''Test'',''solve_linear'']) [BOOL equ, STRING ''z'']              \<comment> \<open>PROG string\<close>
    1.20 +                [''Test'',''solve_linear'']) [BOOL equ, REAL z]              \<comment> \<open>PROG --> as arg\<close>
    1.21    in X) "
    1.22  *)
    1.23  setup \<open>KEStore_Elems.add_mets