diff -r 3e904f8ec16c -r 28b67cae58c3 src/Tools/isac/Knowledge/EqSystem.thy
--- a/src/Tools/isac/Knowledge/EqSystem.thy	Wed Nov 21 12:32:54 2018 +0100
+++ b/src/Tools/isac/Knowledge/EqSystem.thy	Wed Nov 28 11:46:00 2018 +0100
@@ -516,7 +516,7 @@
 
 (**methods**)
 setup \<open>KEStore_Elems.add_mets
-  [Specify.prep_met thy "met_eqsys" [] Celem.e_metID
+    [Specify.prep_met thy "met_eqsys" [] Celem.e_metID
 	    (["EqSystem"], [],
 	      {rew_ord'="tless_true", rls' = Rule.Erls, calc = [], srls = Rule.Erls, prls = Rule.Erls, crls = Rule.Erls,
           errpats = [], nrls = Rule.Erls},
@@ -525,8 +525,10 @@
       (["EqSystem","top_down_substitution"], [],
         {rew_ord'="tless_true", rls' = Rule.Erls, calc = [], srls = Rule.Erls, prls = Rule.Erls, crls = Rule.Erls,
           errpats = [], nrls = Rule.Erls},
-       "empty_script"),
-    Specify.prep_met thy "met_eqsys_topdown_2x2" [] Celem.e_metID
+       "empty_script")]
+\<close>
+setup \<open>KEStore_Elems.add_mets
+    [Specify.prep_met thy "met_eqsys_topdown_2x2" [] Celem.e_metID
       (["EqSystem", "top_down_substitution", "2x2"],
         [("#Given", ["equalities e_s", "solveForVars v_s"]),
           ("#Where",
@@ -571,13 +573,17 @@
           "                              isolate_bdvs False))              @@   " ^
           "       (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^
           "                                  simplify_System False))) e__s)"
-          ---------------------------------------------------------------------------*)),
-    Specify.prep_met thy "met_eqsys_norm" [] Celem.e_metID
+          ---------------------------------------------------------------------------*))]
+\<close>
+setup \<open>KEStore_Elems.add_mets
+    [Specify.prep_met thy "met_eqsys_norm" [] Celem.e_metID
 	    (["EqSystem", "normalise"], [],
 	      {rew_ord'="tless_true", rls' = Rule.Erls, calc = [], srls = Rule.Erls, prls = Rule.Erls, crls = Rule.Erls,
           errpats = [], nrls = Rule.Erls},
-	      "empty_script"),
-    Specify.prep_met thy "met_eqsys_norm_2x2" [] Celem.e_metID
+	      "empty_script")]
+\<close>
+setup \<open>KEStore_Elems.add_mets
+    [Specify.prep_met thy "met_eqsys_norm_2x2" [] Celem.e_metID
 	    (["EqSystem","normalise","2x2"],
 	      [("#Given" ,["equalities e_s", "solveForVars v_s"]),
 		      ("#Find"  ,["solution ss'''"])],
@@ -597,8 +603,10 @@
           "                                  simplify_System_parenthesized False)) @@  " ^
           "               (Try (Rewrite_Set order_system False))) e_s                  " ^
           "   in (SubProblem (EqSystem',[LINEAR,system],[no_met])                      " ^
-          "                  [BOOL_LIST e__s, REAL_LIST v_s]))"),
-    Specify.prep_met thy "met_eqsys_norm_4x4" [] Celem.e_metID
+          "                  [BOOL_LIST e__s, REAL_LIST v_s]))")]
+\<close>
+setup \<open>KEStore_Elems.add_mets
+    [Specify.prep_met thy "met_eqsys_norm_4x4" [] Celem.e_metID
 	      (["EqSystem","normalise","4x4"],
 	       [("#Given" ,["equalities e_s", "solveForVars v_s"]),
 	         ("#Find"  ,["solution ss'''"])],
@@ -624,8 +632,10 @@
            "                             simplify_System_parenthesized False))    @@    " ^
            "      (Try (Rewrite_Set order_system False)))                           e_s " ^
            "   in (SubProblem (EqSystem',[LINEAR,system],[no_met])                      " ^
-           "                  [BOOL_LIST e__s, REAL_LIST v_s]))"),
-    Specify.prep_met thy "met_eqsys_topdown_4x4" [] Celem.e_metID
+           "                  [BOOL_LIST e__s, REAL_LIST v_s]))")]
+\<close>
+setup \<open>KEStore_Elems.add_mets
+    [Specify.prep_met thy "met_eqsys_topdown_4x4" [] Celem.e_metID
 	    (["EqSystem","top_down_substitution","4x4"],
 	      [("#Given" ,["equalities e_s", "solveForVars v_s"]),
 	        ("#Where" , (*accepts missing variables up to diagonal form*)