1.1 --- a/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy	Sun Feb 12 22:57:17 2012 +0100
     1.2 +++ b/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy	Mon Feb 13 17:40:30 2012 +0100
     1.3 @@ -11,12 +11,14 @@
     1.4    rule1: "1 = \<delta>[n]" and
     1.5    rule2: "|| z || > 1 ==> z / (z - 1) = u [n]" and
     1.6    rule3: "|| z || < 1 ==> z / (z - 1) = -u [-n - 1]" and 
     1.7 -  rule4: "|| z || > || \<alpha> || ==> z / (z - \<alpha>) = \<alpha>^^^n * u [n]" and
     1.8 +  rule4: "c * (z / (z - \<alpha>)) = c * \<alpha>^^^n * u [n]" and
     1.9    rule5: "|| z || < || \<alpha> || ==> z / (z - \<alpha>) = -(\<alpha>^^^n) * u [-n - 1]" and
    1.10 -  rule6: "|| z || > 1 ==> z/(z - 1)^^^2 = n * u [n]"
    1.11 +  rule6: "|| z || > 1 ==> z/(z - 1)^^^2 = n * u [n]" (*and
    1.12 +  rule42: "(a * (z/(z-b)) + c * (z/(z-d))) = (a * b^^^n * u [n] + c * d^^^n * u [n])"*)
    1.13  
    1.14  axiomatization where
    1.15 -  ruleZY: "(X z = a / b) = (X' z = a / (z * b))" 
    1.16 +  ruleZY: "(X z = a / b) = (X' z = a / (z * b))" and
    1.17 +  ruleYZ: "(a/b + c/d) = (a*(z/b) + c*(z/d))" 
    1.18  
    1.19  subsection{*Define the Field Descriptions for the specification*}
    1.20  consts
    1.21 @@ -29,12 +31,8 @@
    1.22    Rls {id = "inverse_z", preconds = [], rew_ord = ("dummy_ord",dummy_ord), 
    1.23  	  erls = Erls, srls = Erls, calc = [],
    1.24  	  rules = 
    1.25 -	   [Thm ("rule1",num_str @{thm rule1}),
    1.26 -    Thm ("rule2",num_str @{thm rule2}),
    1.27 -    Thm ("rule3",num_str @{thm rule3}),
    1.28 -    Thm ("rule4",num_str @{thm rule4}),
    1.29 -    Thm ("rule5",num_str @{thm rule5}),
    1.30 -    Thm ("rule6",num_str @{thm rule6})
    1.31 +	   [
    1.32 +    Thm ("rule4",num_str @{thm rule4})
    1.33  	   ], 
    1.34  	 scr = EmptyScr}:rls);
    1.35  *}

     2.1 --- a/src/Tools/isac/Knowledge/Partial_Fractions.thy	Sun Feb 12 22:57:17 2012 +0100
     2.2 +++ b/src/Tools/isac/Knowledge/Partial_Fractions.thy	Mon Feb 13 17:40:30 2012 +0100
     2.3 @@ -50,7 +50,7 @@
     2.4    in HOLogic.mk_binop "Groups.times_class.times" (minus_1, t) end;
     2.5  fun fac_from_sol s =
     2.6    let val (lhs, rhs) = HOLogic.dest_eq s
     2.7 -  in HOLogic.mk_binop "Groups.plus_class.plus" (lhs, flip_sign rhs) end;
     2.8 +  in HOLogic.mk_binop "Groups.minus_class.minus" (lhs, rhs) end;
     2.9  *}
    2.10  
    2.11  ML {*

     3.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy	Sun Feb 12 22:57:17 2012 +0100
     3.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy	Mon Feb 13 17:40:30 2012 +0100
     3.3 @@ -278,7 +278,7 @@
     3.4    in HOLogic.mk_binop "Groups.times_class.times" (minus_1, t) end;
     3.5  fun fac_from_sol s =
     3.6    let val (lhs, rhs) = HOLogic.dest_eq s
     3.7 -  in HOLogic.mk_binop "Groups.plus_class.plus" (lhs, flip_sign rhs) end;
     3.8 +  in HOLogic.mk_binop "Groups.minus_class.minus" (lhs, rhs) end;
     3.9  *}
    3.10  ML {*
    3.11  e_term
    3.12 @@ -855,11 +855,13 @@
    3.13        "      pbz = ((Substitute [A=a]) pbz);"^
    3.14        "      pbz = ((Substitute [B=b]) pbz);"^
    3.15  
    3.16 -(*      "      pbz = Rewrite ruleYZ False pbz;"^*)
    3.17 +      "      pbz = Rewrite ruleYZ False pbz;"^
    3.18 +      "      pbz = drop_questionmarks pbz;"^
    3.19  
    3.20 -      "      (pbz1::real) = Take pbz;"^
    3.21 -"(pbz2::real) = (Rewrite_Set inverse_z False) pbz1;"^
    3.22 -      "      (n_eq::bool) = Take (X_n = pbz2)"^ 
    3.23 +      "      (iztrans::real) = Take pbz;"^
    3.24 +      "      iztrans = (Rewrite_Set inverse_z False) iztrans;"^
    3.25 +      "      iztrans = drop_questionmarks iztrans;"^
    3.26 +      "      (n_eq::bool) = Take (X_n = iztrans)"^ 
    3.27  
    3.28        "  in n_eq)" 
    3.29        ));
    3.30 @@ -1092,6 +1094,10 @@
    3.31  val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    3.32  *}
    3.33  
    3.34 +ML {*
    3.35 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    3.36 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
    3.37 +*}
    3.38  
    3.39  ML {*
    3.40  trace_script := true;