1.1 --- a/doc-src/isac/jrocnik/Test_Z_Transform.thy	Mon Sep 05 12:40:23 2011 +0200
     1.2 +++ b/doc-src/isac/jrocnik/Test_Z_Transform.thy	Mon Sep 05 14:43:38 2011 +0200
     1.3 @@ -185,6 +185,9 @@
     1.4  val SOME (eq3'' ,_) = rewrite_set_ @{theory Isac} false norm_Rational eq3';
     1.5  term2str eq3'';
     1.6  *}
     1.7 +
     1.8 +subsubsection {*get first koeffizient*}
     1.9 +
    1.10  ML {*
    1.11  val SOME (eq4_1,_) = rewrite_terms_ @{theory Isac} e_rew_ord e_rls [s_1] eq3'';
    1.12  term2str eq4_1;
    1.13 @@ -229,10 +232,59 @@
    1.14  *}
    1.15  ML {*
    1.16  val (p,_,f,nxt,_,pt) = me nxt p [] pt; 
    1.17 -f2str f
    1.18 +f2str f;
    1.19  *}
    1.20 +
    1.21 +subsubsection {*get second koeffizient*}
    1.22 +
    1.23  ML {*
    1.24 +val SOME (eq4b_1,_) = rewrite_terms_ @{theory Isac} e_rew_ord e_rls [s_2] eq3'';
    1.25 +term2str eq4_1;
    1.26 +*}
    1.27 +
    1.28 +ML {*
    1.29 +val SOME (eq4b_2,_) = rewrite_set_ @{theory Isac} false norm_Rational eq4b_1;
    1.30 +term2str eq4b_2;
    1.31 +*}
    1.32 +
    1.33 +ML {*
    1.34 +val fmz = ["equality (3 = -3 * B / (4::real))", "solveFor B","solutions L"];
    1.35 +val (dI',pI',mI') =("Isac", ["univariate","equation"], ["no_met"]);
    1.36 +
    1.37 +val (p,_,fb,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
    1.38 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
    1.39 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
    1.40 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
    1.41 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
    1.42 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
    1.43 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
    1.44 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
    1.45 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
    1.46 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
    1.47 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
    1.48 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
    1.49 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
    1.50 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
    1.51 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
    1.52 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
    1.53 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
    1.54 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
    1.55 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
    1.56 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
    1.57 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
    1.58 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
    1.59 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
    1.60 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
    1.61 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
    1.62 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
    1.63 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
    1.64 +val (p,_,fb,nxt,_,pt) = me nxt p [] pt; 
    1.65 +f2str fb;
    1.66 +*}
    1.67 +
    1.68 +ML {* (*check koeffizients*)
    1.69  if f2str f = "[A = 4]" then () else error "part.fract. eq4_1";
    1.70 +if f2str fb = "[B = -4]" then () else error "part.fract. eq4_1";
    1.71  *}
    1.72  
    1.73  end