1.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy	Mon Aug 26 09:20:07 2019 +0200
     1.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy	Mon Aug 26 17:40:27 2019 +0200
     1.3 @@ -261,7 +261,7 @@
     1.4    val fmz = ["equality (z^^^2 - 1/4*z - 1/8 = (0::real))",
     1.5               "solveFor z",
     1.6               "solutions L"];
     1.7 -  val (dI',pI',mI') =("Isac", ["univariate","equation"], ["no_met"]);
     1.8 +  val (dI',pI',mI') =("Isac_Knowledge", ["univariate","equation"], ["no_met"]);
     1.9  \<close>
    1.10  text \<open>\noindent Check if the given equation matches the specification of this
    1.11          equation type.\<close>
    1.12 @@ -273,7 +273,7 @@
    1.13         equation with a more specific type definition.\<close>
    1.14  
    1.15  ML \<open>
    1.16 -  Context.theory_name thy = "Isac";
    1.17 +  Context.theory_name thy = "Isac_Knowledge";
    1.18    val denominator = TermC.parseNEW ctxt "-1 + -2 * z + 8 * z ^^^ 2 = 0";
    1.19    val fmz =                                             (*specification*)
    1.20      ["equality (-1 + -2 * z + 8 * z ^^^ 2 = (0::real))",(*equality*)
    1.21 @@ -281,7 +281,7 @@
    1.22       "solutions L"];                                    (*identifier for
    1.23                                                            solution*)
    1.24    val (dI',pI',mI') =
    1.25 -    ("Isac", 
    1.26 +    ("Isac_Knowledge", 
    1.27        ["abcFormula","degree_2","polynomial","univariate","equation"],
    1.28        ["no_met"]);
    1.29  \<close>
    1.30 @@ -597,7 +597,7 @@
    1.31        expression 2nd order. Follow up the calculation in 
    1.32        Section~\ref{sec:calc:ztrans} Step~03.\<close>
    1.33  
    1.34 -ML \<open>Context.theory_name thy = "Isac"\<close>
    1.35 +ML \<open>Context.theory_name thy = "Isac_Knowledge"\<close>
    1.36  
    1.37  text\<open>\noindent We define two axiomatization, the first one is the main ansatz,
    1.38        the next one is just an equivalent transformation of the resulting
    1.39 @@ -686,7 +686,7 @@
    1.40  
    1.41  text\<open>\noindent Still working at {\sisac}\ldots\<close>
    1.42  
    1.43 -ML \<open>Context.theory_name thy = "Isac"\<close>
    1.44 +ML \<open>Context.theory_name thy = "Isac_Knowledge"\<close>
    1.45  
    1.46  subsubsection \<open>Build a Rule-Set for the Ansatz\<close>
    1.47  text \<open>\noindent The \emph{ansatz} rules violate the principle that each
    1.48 @@ -739,7 +739,7 @@
    1.49    term2str eq4_2;
    1.50  
    1.51    val fmz = ["equality (3=3*A/(4::real))", "solveFor A","solutions L"];
    1.52 -  val (dI',pI',mI') =("Isac", ["univariate","equation"], ["no_met"]);
    1.53 +  val (dI',pI',mI') =("Isac_Knowledge", ["univariate","equation"], ["no_met"]);
    1.54    (*
    1.55     * Solve the simple linear equation for A:
    1.56     * Return eq, not list of eq's
    1.57 @@ -752,7 +752,7 @@
    1.58    val (p,_,fa,nxt,_,pt) = me nxt p [] pt; 
    1.59      (*Add_Find "solutions L"*)
    1.60    val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
    1.61 -    (*Specify_Theory "Isac"*)
    1.62 +    (*Specify_Theory "Isac_Knowledge"*)
    1.63    val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
    1.64      (*Specify_Problem ["normalise","polynomial",
    1.65                         "univariate","equation"])*)
    1.66 @@ -819,7 +819,7 @@
    1.67    term2str eq4b_2;
    1.68  
    1.69    val fmz = ["equality (3= -3*B/(4::real))", "solveFor B","solutions L"];
    1.70 -  val (dI',pI',mI') =("Isac", ["univariate","equation"], ["no_met"]);
    1.71 +  val (dI',pI',mI') =("Isac_Knowledge", ["univariate","equation"], ["no_met"]);
    1.72    val (p,_,fb,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
    1.73    val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
    1.74    val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
    1.75 @@ -1214,7 +1214,7 @@
    1.76      ["filterExpression (X  = 3 / (z - 1/4 + -1/8 * (1/(z::real))))",
    1.77       "stepResponse (x[n::real]::bool)"];
    1.78    val (dI,pI,mI) = 
    1.79 -    ("Isac", ["Inverse", "Z_Transform", "SignalProcessing"], 
    1.80 +    ("Isac_Knowledge", ["Inverse", "Z_Transform", "SignalProcessing"], 
    1.81               ["SignalProcessing","Z_Transform","Inverse"]);
    1.82  
    1.83    val ([
    1.84 @@ -1256,7 +1256,7 @@
    1.85       "stepResponse (x[n::real]::bool)"];
    1.86       
    1.87    val (dI,pI,mI) =
    1.88 -    ("Isac", ["Inverse", "Z_Transform", "SignalProcessing"], 
    1.89 +    ("Isac_Knowledge", ["Inverse", "Z_Transform", "SignalProcessing"], 
    1.90               ["SignalProcessing","Z_Transform","Inverse"]);
    1.91               
    1.92    val (p,_,f,nxt,_,pt)  = CalcTreeTEST [(fmz, (dI,pI,mI))];
    1.93 @@ -1423,7 +1423,7 @@
    1.94    val (p,_,f,nxt,_,pt) = me nxt p [] pt; 
    1.95      (*Rewrite_Set "polyeq_simplify"*)
    1.96    val (p,_,f,nxt,_,pt) = me nxt p [] pt; 
    1.97 -    (*Subproblem("Isac",["degree_1","polynomial","univariate","equation"])*)
    1.98 +    (*Subproblem("Isac_Knowledge",["degree_1","polynomial","univariate","equation"])*)
    1.99    val (p,_,f,nxt,_,pt) = me nxt p [] pt;
   1.100    val (p,_,f,nxt,_,pt) = me nxt p [] pt;
   1.101    val (p,_,f,nxt,_,pt) = me nxt p [] pt;
   1.102 @@ -1603,7 +1603,7 @@
   1.103        \end{verbatim}
   1.104        \item We check if the \textbf{semantics of the program} by stepwise evaluation
   1.105          of the program. Evaluation is done by the Lucas-Interpreter, which works
   1.106 -        using the knowledge in theory Isac; so we have to re-build Isac. And the
   1.107 +        using the knowledge in theory Isac_Knowledge; so we have to re-build Isac. And the
   1.108          test are performed simplest in a file which is loaded with Isac.
   1.109          See \ttfamily tests/../partial\_fractions.sml \normalfont.
   1.110    \end{enumerate}