diff -r 7e314dd233fd -r 46fe5a8c3911 test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy
--- a/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy	Tue May 19 12:33:35 2020 +0200
+++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy	Wed May 20 12:52:09 2020 +0200
@@ -261,12 +261,12 @@
   val fmz = ["equality (z^^^2 - 1/4*z - 1/8 = (0::real))",
              "solveFor z",
              "solutions L"];
-  val (dI',pI',mI') =("Isac_Knowledge", ["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>
 ML \<open>
-  M_Match.match_pbl fmz (Problem.from_store ["univariate","equation"]);
+  M_Match.match_pbl fmz (Problem.from_store ["univariate", "equation"]);
 \<close>
 
 text\<open>\noindent We switch up to the {\sisac} Context and try to solve the 
@@ -282,7 +282,7 @@
                                                           solution*)
   val (dI',pI',mI') =
     ("Isac_Knowledge", 
-      ["abcFormula","degree_2","polynomial","univariate","equation"],
+      ["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
       ["no_met"]);
 \<close>
 
@@ -291,7 +291,7 @@
         
 ML \<open>
   M_Match.match_pbl fmz (Problem.from_store
-    ["abcFormula","degree_2","polynomial","univariate","equation"]);
+    ["abcFormula", "degree_2", "polynomial", "univariate", "equation"]);
 \<close>
 
 text \<open>\noindent We stepwise solve the equation. This is done by the
@@ -738,8 +738,8 @@
     rewrite_set_ @{theory} false norm_Rational eq4_1;
   UnparseC.term eq4_2;
 
-  val fmz = ["equality (3=3*A/(4::real))", "solveFor A","solutions L"];
-  val (dI',pI',mI') =("Isac_Knowledge", ["univariate","equation"], ["no_met"]);
+  val fmz = ["equality (3=3*A/(4::real))", "solveFor A", "solutions L"];
+  val (dI',pI',mI') =("Isac_Knowledge", ["univariate", "equation"], ["no_met"]);
   (*
    * Solve the simple linear equation for A:
    * Return eq, not list of eq's
@@ -754,14 +754,14 @@
   val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
     (*Specify_Theory "Isac_Knowledge"*)
   val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
-    (*Specify_Problem ["normalise","polynomial",
-                       "univariate","equation"])*)
+    (*Specify_Problem ["normalise", "polynomial",
+                       "univariate", "equation"])*)
   val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
-    (* Specify_Method["PolyEq","normalise_poly"]*)
+    (* Specify_Method["PolyEq", "normalise_poly"]*)
   val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
-    (*Apply_Method["PolyEq","normalise_poly"]*)
+    (*Apply_Method["PolyEq", "normalise_poly"]*)
   val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
-    (*Rewrite ("all_left","PolyEq.all_left")*)
+    (*Rewrite ("all_left", "PolyEq.all_left")*)
   val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
     (*Rewrite_Set_Inst(["(''bdv'',A)"],"make_ratpoly_in")*)
   val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
@@ -778,7 +778,7 @@
   val (p,_,fa,nxt,_,pt) = me nxt p [] pt; 
   val (p,_,fa,nxt,_,pt) = me nxt p [] pt; 
   val (p,_,fa,nxt,_,pt) = me nxt p [] pt; 
-    (*Apply_Method ["PolyEq","solve_d1_polyeq_equation"]*)
+    (*Apply_Method ["PolyEq", "solve_d1_polyeq_equation"]*)
   val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
     (*Rewrite_Set_Inst(["(''bdv'',A)"],"d1_polyeq_simplify")*)
   val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
@@ -790,11 +790,11 @@
   val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
     (*Check_elementwise "Assumptions"*)
   val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
-    (*Check_Postcond ["degree_1","polynomial",
-                      "univariate","equation"]*)
+    (*Check_Postcond ["degree_1", "polynomial",
+                      "univariate", "equation"]*)
   val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
-    (*Check_Postcond ["normalise","polynomial",
-                      "univariate","equation"]*)
+    (*Check_Postcond ["normalise", "polynomial",
+                      "univariate", "equation"]*)
   val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
     (*End_Proof'*)
   f2str fa;
@@ -818,8 +818,8 @@
     rewrite_set_ @{theory} false norm_Rational eq4b_1;
   UnparseC.term eq4b_2;
 
-  val fmz = ["equality (3= -3*B/(4::real))", "solveFor B","solutions L"];
-  val (dI',pI',mI') =("Isac_Knowledge", ["univariate","equation"], ["no_met"]);
+  val fmz = ["equality (3= -3*B/(4::real))", "solveFor B", "solutions L"];
+  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;
@@ -885,7 +885,7 @@
 setup \<open>KEStore_Elems.add_pbts
   [Problem.prep_input thy "pbl_SP" [] Problem.id_empty (["SignalProcessing"], [], Rule_Set.empty, NONE, []),
     Problem.prep_input thy "pbl_SP_Ztrans" [] Problem.id_empty
-      (["Z_Transform","SignalProcessing"], [], Rule_Set.empty, NONE, [])]\<close>
+      (["Z_Transform", "SignalProcessing"], [], Rule_Set.empty, NONE, [])]\<close>
 
 text\<open>\noindent For the suddenly created node we have to define the input
        and output parameters. We already prepared their definition in
@@ -898,10 +898,10 @@
           ("#Find", ["stepResponse n_eq"])],
         Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)],
         NONE,
-        [["SignalProcessing","Z_Transform","Inverse"]])]\<close>
+        [["SignalProcessing", "Z_Transform", "Inverse"]])]\<close>
 ML \<open>
   Test_Tool.show_ptyps() ();
-  Problem.from_store ["Inverse","Z_Transform","SignalProcessing"];
+  Problem.from_store ["Inverse", "Z_Transform", "SignalProcessing"];
 \<close>
 
 subsection \<open>Define Name and Signature for the Method\<close>
@@ -974,7 +974,7 @@
       the hierarchy.\<close>
 
 ML \<open>
-  Method.from_store ["SignalProcessing","Z_Transform","Inverse"];
+  Method.from_store ["SignalProcessing", "Z_Transform", "Inverse"];
 \<close>
 
 section \<open>Program in TP-based language \label{prog-steps}\<close>
@@ -1210,7 +1210,7 @@
      "stepResponse (x[n::real]::bool)"];
   val (dI,pI,mI) = 
     ("Isac_Knowledge", ["Inverse", "Z_Transform", "SignalProcessing"], 
-             ["SignalProcessing","Z_Transform","Inverse"]);
+             ["SignalProcessing", "Z_Transform", "Inverse"]);
 
   val ([
           (
@@ -1252,7 +1252,7 @@
      
   val (dI,pI,mI) =
     ("Isac_Knowledge", ["Inverse", "Z_Transform", "SignalProcessing"], 
-             ["SignalProcessing","Z_Transform","Inverse"]);
+             ["SignalProcessing", "Z_Transform", "Inverse"]);
              
   val (p,_,f,nxt,_,pt)  = CalcTreeTEST [(fmz, (dI,pI,mI))];
   val (p,_,f,nxt,_,pt) = me nxt p [] pt; 
@@ -1406,7 +1406,7 @@
   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;
-    (*Specify_Problem ["normalise","polynomial","univariate","equation"]*)
+    (*Specify_Problem ["normalise", "polynomial", "univariate", "equation"]*)
   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
     (*Specify_Method ["PolyEq", "normalise_poly"]*)
   val (p,_,f,nxt,_,pt) = me nxt p [] pt;
@@ -1418,7 +1418,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_Knowledge",["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;