diff -r a2b0b338d966 -r 99c8d2ff63eb test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy
--- a/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy	Mon Aug 26 09:20:07 2019 +0200
+++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy	Mon Aug 26 17:40:27 2019 +0200
@@ -261,7 +261,7 @@
   val fmz = ["equality (z^^^2 - 1/4*z - 1/8 = (0::real))",
              "solveFor z",
              "solutions L"];
-  val (dI',pI',mI') =("Isac", ["univariate","equation"], ["no_met"]);
+  val (dI',pI',mI') =("Isac_Knowledge", ["univariate","equation"], ["no_met"]);
 \<close>
 text \<open>\noindent Check if the given equation matches the specification of this
         equation type.\<close>
@@ -273,7 +273,7 @@
        equation with a more specific type definition.\<close>
 
 ML \<open>
-  Context.theory_name thy = "Isac";
+  Context.theory_name thy = "Isac_Knowledge";
   val denominator = TermC.parseNEW ctxt "-1 + -2 * z + 8 * z ^^^ 2 = 0";
   val fmz =                                             (*specification*)
     ["equality (-1 + -2 * z + 8 * z ^^^ 2 = (0::real))",(*equality*)
@@ -281,7 +281,7 @@
      "solutions L"];                                    (*identifier for
                                                           solution*)
   val (dI',pI',mI') =
-    ("Isac", 
+    ("Isac_Knowledge", 
       ["abcFormula","degree_2","polynomial","univariate","equation"],
       ["no_met"]);
 \<close>
@@ -597,7 +597,7 @@
       expression 2nd order. Follow up the calculation in 
       Section~\ref{sec:calc:ztrans} Step~03.\<close>
 
-ML \<open>Context.theory_name thy = "Isac"\<close>
+ML \<open>Context.theory_name thy = "Isac_Knowledge"\<close>
 
 text\<open>\noindent We define two axiomatization, the first one is the main ansatz,
       the next one is just an equivalent transformation of the resulting
@@ -686,7 +686,7 @@
 
 text\<open>\noindent Still working at {\sisac}\ldots\<close>
 
-ML \<open>Context.theory_name thy = "Isac"\<close>
+ML \<open>Context.theory_name thy = "Isac_Knowledge"\<close>
 
 subsubsection \<open>Build a Rule-Set for the Ansatz\<close>
 text \<open>\noindent The \emph{ansatz} rules violate the principle that each
@@ -739,7 +739,7 @@
   term2str eq4_2;
 
   val fmz = ["equality (3=3*A/(4::real))", "solveFor A","solutions L"];
-  val (dI',pI',mI') =("Isac", ["univariate","equation"], ["no_met"]);
+  val (dI',pI',mI') =("Isac_Knowledge", ["univariate","equation"], ["no_met"]);
   (*
    * Solve the simple linear equation for A:
    * Return eq, not list of eq's
@@ -752,7 +752,7 @@
   val (p,_,fa,nxt,_,pt) = me nxt p [] pt; 
     (*Add_Find "solutions L"*)
   val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
-    (*Specify_Theory "Isac"*)
+    (*Specify_Theory "Isac_Knowledge"*)
   val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
     (*Specify_Problem ["normalise","polynomial",
                        "univariate","equation"])*)
@@ -819,7 +819,7 @@
   term2str eq4b_2;
 
   val fmz = ["equality (3= -3*B/(4::real))", "solveFor B","solutions L"];
-  val (dI',pI',mI') =("Isac", ["univariate","equation"], ["no_met"]);
+  val (dI',pI',mI') =("Isac_Knowledge", ["univariate","equation"], ["no_met"]);
   val (p,_,fb,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
   val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
   val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
@@ -1214,7 +1214,7 @@
     ["filterExpression (X  = 3 / (z - 1/4 + -1/8 * (1/(z::real))))",
      "stepResponse (x[n::real]::bool)"];
   val (dI,pI,mI) = 
-    ("Isac", ["Inverse", "Z_Transform", "SignalProcessing"], 
+    ("Isac_Knowledge", ["Inverse", "Z_Transform", "SignalProcessing"], 
              ["SignalProcessing","Z_Transform","Inverse"]);
 
   val ([
@@ -1256,7 +1256,7 @@
      "stepResponse (x[n::real]::bool)"];
      
   val (dI,pI,mI) =
-    ("Isac", ["Inverse", "Z_Transform", "SignalProcessing"], 
+    ("Isac_Knowledge", ["Inverse", "Z_Transform", "SignalProcessing"], 
              ["SignalProcessing","Z_Transform","Inverse"]);
              
   val (p,_,f,nxt,_,pt)  = CalcTreeTEST [(fmz, (dI,pI,mI))];
@@ -1423,7 +1423,7 @@
   val (p,_,f,nxt,_,pt) = me nxt p [] pt; 
     (*Rewrite_Set "polyeq_simplify"*)
   val (p,_,f,nxt,_,pt) = me nxt p [] pt; 
-    (*Subproblem("Isac",["degree_1","polynomial","univariate","equation"])*)
+    (*Subproblem("Isac_Knowledge",["degree_1","polynomial","univariate","equation"])*)
   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
@@ -1603,7 +1603,7 @@
       \end{verbatim}
       \item We check if the \textbf{semantics of the program} by stepwise evaluation
         of the program. Evaluation is done by the Lucas-Interpreter, which works
-        using the knowledge in theory Isac; so we have to re-build Isac. And the
+        using the knowledge in theory Isac_Knowledge; so we have to re-build Isac. And the
         test are performed simplest in a file which is loaded with Isac.
         See \ttfamily tests/../partial\_fractions.sml \normalfont.
   \end{enumerate}