diff -r 7e314dd233fd -r 46fe5a8c3911 src/Tools/isac/Knowledge/EqSystem.thy
--- a/src/Tools/isac/Knowledge/EqSystem.thy	Tue May 19 12:33:35 2020 +0200
+++ b/src/Tools/isac/Knowledge/EqSystem.thy	Wed May 20 12:52:09 2020 +0200
@@ -85,7 +85,7 @@
 ML \<open>
 (** rewrite order 'ord_simplify_System' **)
 
-(* order wrt. several linear (i.e. without exponents) variables "c","c_2",..
+(* order wrt. several linear (i.e. without exponents) variables "c", "c_2",..
    which leaves the monomials containing c, c_2,... at the end of an Integral
    and puts the c, c_2,... rightmost within a monomial.
 
@@ -436,14 +436,14 @@
             ["(tl v_s) from v_s occur_exactly_in (NTH 1 (e_s::bool list))",
               "    v_s  from v_s occur_exactly_in (NTH 2 (e_s::bool list))"]),
           ("#Find"  ,["solution ss'''"])],
-        prls_triangular, SOME "solveSystem e_s v_s", [["EqSystem","top_down_substitution","2x2"]])),
+        prls_triangular, SOME "solveSystem e_s v_s", [["EqSystem", "top_down_substitution", "2x2"]])),
     (Problem.prep_input thy "pbl_equsys_lin_2x2_norm" [] Problem.id_empty
       (["normalise", "2x2", "LINEAR", "system"],
         [("#Given" ,["equalities e_s", "solveForVars v_s"]),
           ("#Find"  ,["solution ss'''"])],
       Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)], 
       SOME "solveSystem e_s v_s", 
-      [["EqSystem","normalise","2x2"]])),
+      [["EqSystem", "normalise", "2x2"]])),
     (Problem.prep_input thy "pbl_equsys_lin_3x3" [] Problem.id_empty
       (["3x3", "LINEAR", "system"],
         (*~~~~~~~~~~~~~~~~~~~~~~~~~*)
@@ -480,7 +480,7 @@
       Rule_Set.append_rules "prls_tri_4x4_lin_sys" prls_triangular
 	      [Rule.Eval ("Prog_Expr.occurs'_in", Prog_Expr.eval_occurs_in "")], 
       SOME "solveSystem e_s v_s", 
-      [["EqSystem","top_down_substitution","4x4"]])),
+      [["EqSystem", "top_down_substitution", "4x4"]])),
     (Problem.prep_input thy "pbl_equsys_lin_4x4_norm" [] Problem.id_empty
       (["normalise", "4x4", "LINEAR", "system"],
         [("#Given" ,["equalities e_s", "solveForVars v_s"]),
@@ -488,7 +488,7 @@
           ("#Find"  ,["solution ss'''"])],
         Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)], 
         SOME "solveSystem e_s v_s", 
-        [["EqSystem","normalise","4x4"]]))]\<close>
+        [["EqSystem", "normalise", "4x4"]]))]\<close>
 
 ML \<open>
 (*this is for NTH only*)
@@ -516,7 +516,7 @@
           errpats = [], nrls = Rule_Set.Empty},
 	      @{thm refl}),
     Method.prep_input thy "met_eqsys_topdown" [] Method.id_empty
-      (["EqSystem","top_down_substitution"], [],
+      (["EqSystem", "top_down_substitution"], [],
         {rew_ord'="tless_true", rls' = Rule_Set.Empty, calc = [], srls = Rule_Set.Empty, prls = Rule_Set.Empty, crls = Rule_Set.Empty,
           errpats = [], nrls = Rule_Set.Empty},
        @{thm refl})]
@@ -581,7 +581,7 @@
       [BOOL_LIST e__s, REAL_LIST v_s])"
 setup \<open>KEStore_Elems.add_mets
     [Method.prep_input thy "met_eqsys_norm_2x2" [] Method.id_empty
-	    (["EqSystem","normalise","2x2"],
+	    (["EqSystem", "normalise", "2x2"],
 	      [("#Given" ,["equalities e_s", "solveForVars v_s"]),
 		      ("#Find"  ,["solution ss'''"])],
 	      {rew_ord'="tless_true", rls' = Rule_Set.Empty, calc = [], 
@@ -613,7 +613,7 @@
       [BOOL_LIST e__s, REAL_LIST v_s])"
 setup \<open>KEStore_Elems.add_mets
     [Method.prep_input thy "met_eqsys_norm_4x4" [] Method.id_empty
-	      (["EqSystem","normalise","4x4"],
+	      (["EqSystem", "normalise", "4x4"],
 	       [("#Given" ,["equalities e_s", "solveForVars v_s"]),
 	         ("#Find"  ,["solution ss'''"])],
 	       {rew_ord'="tless_true", rls' = Rule_Set.Empty, calc = [], 
@@ -622,7 +622,7 @@
 	               Rule.Thm ("tl_Cons",ThmC.numerals_to_Free @{thm tl_Cons}),
 	               Rule.Thm ("tl_Nil",ThmC.numerals_to_Free @{thm tl_Nil})], 
 		       prls = Rule_Set.Empty, crls = Rule_Set.Empty, errpats = [], nrls = Rule_Set.Empty},
-		     (*STOPPED.WN06? met ["EqSystem","normalise","4x4"] #>#>#>#>#>#>#>#>#>#>#>#>#>@*)
+		     (*STOPPED.WN06? met ["EqSystem", "normalise", "4x4"] #>#>#>#>#>#>#>#>#>#>#>#>#>@*)
 		     @{thm solve_system3.simps})]
 \<close>
 
@@ -645,7 +645,7 @@
     [e_1, e_2, NTH 3 e_s, NTH 4 e_s])"
 setup \<open>KEStore_Elems.add_mets
     [Method.prep_input thy "met_eqsys_topdown_4x4" [] Method.id_empty
-	    (["EqSystem","top_down_substitution","4x4"],
+	    (["EqSystem", "top_down_substitution", "4x4"],
 	      [("#Given" ,["equalities e_s", "solveForVars v_s"]),
 	        ("#Where" , (*accepts missing variables up to diagonal form*)
             ["(NTH 1 (v_s::real list)) occurs_in (NTH 1 (e_s::bool list))",