diff -r 9529c8483d00 -r 815b0dc8b589 src/Tools/isac/Knowledge/EqSystem.thy
--- a/src/Tools/isac/Knowledge/EqSystem.thy	Sat Jun 12 18:33:15 2021 +0200
+++ b/src/Tools/isac/Knowledge/EqSystem.thy	Tue Jun 15 22:24:20 2021 +0200
@@ -499,18 +499,13 @@
 
 section \<open>Methods\<close>
 
-setup \<open>KEStore_Elems.add_mets
-    [MethodC.prep_input @{theory} "met_eqsys" [] MethodC.id_empty
-	    (["EqSystem"], [],
-	      {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}),
-    MethodC.prep_input @{theory} "met_eqsys_topdown" [] MethodC.id_empty
-      (["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})]
-\<close>
+method met_eqsys : "EqSystem" =
+  \<open>{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}\<close>
+
+method met_eqsys_topdown : "EqSystem/top_down_substitution" =
+  \<open>{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}\<close>
 
 partial_function (tailrec) solve_system :: "bool list => real list => bool list"
   where
@@ -531,29 +526,24 @@
     e__s = Take [e_1, e_2]                                                       
   in
     Try (Rewrite_Set ''order_system'' ) e__s)                              "
-setup \<open>KEStore_Elems.add_mets
-    [MethodC.prep_input @{theory} "met_eqsys_topdown_2x2" [] MethodC.id_empty
-      (["EqSystem", "top_down_substitution", "2x2"],
-        [("#Given", ["equalities e_s", "solveForVars v_s"]),
-          ("#Where",
-            ["(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'''"])],
-	      {rew_ord'="ord_simplify_System", rls' = Rule_Set.Empty, calc = [], 
-	        srls = Rule_Set.append_rules "srls_top_down_2x2" Rule_Set.empty
-				      [\<^rule_thm>\<open>hd_thm\<close>,
-				        \<^rule_thm>\<open>tl_Cons\<close>,
-				        \<^rule_thm>\<open>tl_Nil\<close>], 
-	        prls = prls_triangular, crls = Rule_Set.Empty, errpats = [], nrls = Rule_Set.Empty},
-	      @{thm solve_system.simps})]
-\<close>
-setup \<open>KEStore_Elems.add_mets
-    [MethodC.prep_input @{theory} "met_eqsys_norm" [] MethodC.id_empty
-	    (["EqSystem", "normalise"], [],
-	      {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})]
-\<close>
+
+method met_eqsys_topdown_2x2 : "EqSystem/top_down_substitution/2x2" =
+  \<open>{rew_ord'="ord_simplify_System", rls' = Rule_Set.Empty, calc = [], 
+    srls = Rule_Set.append_rules "srls_top_down_2x2" Rule_Set.empty
+        [\<^rule_thm>\<open>hd_thm\<close>,
+          \<^rule_thm>\<open>tl_Cons\<close>,
+          \<^rule_thm>\<open>tl_Nil\<close>], 
+    prls = prls_triangular, crls = Rule_Set.Empty, errpats = [], nrls = Rule_Set.Empty}\<close>
+  Program: solve_system.simps
+  Given: "equalities e_s" "solveForVars v_s"
+  Where:
+    "(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'''"
+
+method met_eqsys_norm : "EqSystem/normalise" =
+  \<open>{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}\<close>
 
 partial_function (tailrec) solve_system2 :: "bool list => real list => bool list"
   where
@@ -569,19 +559,17 @@
   in
     SubProblem (''EqSystem'', [''LINEAR'', ''system''], [''no_met''])
       [BOOL_LIST e__s, REAL_LIST v_s])"
-setup \<open>KEStore_Elems.add_mets
-    [MethodC.prep_input @{theory} "met_eqsys_norm_2x2" [] MethodC.id_empty
-	    (["EqSystem", "normalise", "2x2"],
-	      [("#Given" ,["equalities e_s", "solveForVars v_s"]),
-		      ("#Find"  ,["solution ss'''"])],
-	      {rew_ord'="tless_true", rls' = Rule_Set.Empty, calc = [], 
-	        srls = Rule_Set.append_rules "srls_normalise_2x2" Rule_Set.empty
-				      [\<^rule_thm>\<open>hd_thm\<close>,
-				        \<^rule_thm>\<open>tl_Cons\<close>,
-				        \<^rule_thm>\<open>tl_Nil\<close>], 
-		      prls = Rule_Set.Empty, crls = Rule_Set.Empty, errpats = [], nrls = Rule_Set.Empty},
-		    @{thm solve_system2.simps})]
-\<close>
+
+method met_eqsys_norm_2x2 : "EqSystem/normalise/2x2" =
+  \<open>{rew_ord'="tless_true", rls' = Rule_Set.Empty, calc = [], 
+    srls = Rule_Set.append_rules "srls_normalise_2x2" Rule_Set.empty
+        [\<^rule_thm>\<open>hd_thm\<close>,
+          \<^rule_thm>\<open>tl_Cons\<close>,
+          \<^rule_thm>\<open>tl_Nil\<close>], 
+    prls = Rule_Set.Empty, crls = Rule_Set.Empty, errpats = [], nrls = Rule_Set.Empty}\<close>
+  Program: solve_system2.simps
+  Given: "equalities e_s" "solveForVars v_s"
+  Find: "solution ss'''"
 
 partial_function (tailrec) solve_system3 :: "bool list => real list => bool list"
   where
@@ -601,20 +589,17 @@
   in
     SubProblem (''EqSystem'', [''LINEAR'', ''system''], [''no_met''])
       [BOOL_LIST e__s, REAL_LIST v_s])"
-setup \<open>KEStore_Elems.add_mets
-    [MethodC.prep_input @{theory} "met_eqsys_norm_4x4" [] MethodC.id_empty
-	      (["EqSystem", "normalise", "4x4"],
-	       [("#Given" ,["equalities e_s", "solveForVars v_s"]),
-	         ("#Find"  ,["solution ss'''"])],
-	       {rew_ord'="tless_true", rls' = Rule_Set.Empty, calc = [], 
-	         srls = Rule_Set.append_rules "srls_normalise_4x4" srls
-	             [\<^rule_thm>\<open>hd_thm\<close>,
-	               \<^rule_thm>\<open>tl_Cons\<close>,
-	               \<^rule_thm>\<open>tl_Nil\<close>], 
-		       prls = Rule_Set.Empty, crls = Rule_Set.Empty, errpats = [], nrls = Rule_Set.Empty},
-		     (*STOPPED.WN06? met ["EqSystem", "normalise", "4x4"] #>#>#>#>#>#>#>#>#>#>#>#>#>@*)
-		     @{thm solve_system3.simps})]
-\<close>
+
+method met_eqsys_norm_4x4 : "EqSystem/normalise/4x4" =
+  \<open>{rew_ord'="tless_true", rls' = Rule_Set.Empty, calc = [],
+    srls =
+      Rule_Set.append_rules "srls_normalise_4x4" srls
+        [\<^rule_thm>\<open>hd_thm\<close>, \<^rule_thm>\<open>tl_Cons\<close>, \<^rule_thm>\<open>tl_Nil\<close>],
+    prls = Rule_Set.Empty, crls = Rule_Set.Empty, errpats = [], nrls = Rule_Set.Empty}\<close>
+  Program: solve_system3.simps
+  Given: "equalities e_s" "solveForVars v_s"
+  Find: "solution ss'''"
+  (*STOPPED.WN06? met ["EqSystem", "normalise", "4x4"] #>#>#>#>#>#>#>#>#>#>#>#>#>@*)
 
 partial_function (tailrec) solve_system4 :: "bool list => real list => bool list"
   where
@@ -633,24 +618,24 @@
       ) e_2
   in
     [e_1, e_2, NTH 3 e_s, NTH 4 e_s])"
-setup \<open>KEStore_Elems.add_mets
-    [MethodC.prep_input @{theory} "met_eqsys_topdown_4x4" [] MethodC.id_empty
-	    (["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))",
-              "(NTH 2 (v_s::real list)) occurs_in (NTH 2 (e_s::bool list))",
-              "(NTH 3 (v_s::real list)) occurs_in (NTH 3 (e_s::bool list))",
-              "(NTH 4 (v_s::real list)) occurs_in (NTH 4 (e_s::bool list))"]),
-	        ("#Find", ["solution ss'''"])],
-	    {rew_ord'="ord_simplify_System", rls' = Rule_Set.Empty, calc = [], 
-	      srls = Rule_Set.append_rules "srls_top_down_4x4" srls [], 
-	      prls = Rule_Set.append_rules "prls_tri_4x4_lin_sys" prls_triangular
-			      [\<^rule_eval>\<open>Prog_Expr.occurs_in\<close> (Prog_Expr.eval_occurs_in "")], 
-	      crls = Rule_Set.Empty, errpats = [], nrls = Rule_Set.Empty},
-	    (*FIXXXXME.WN060916: this script works ONLY for exp 7.79 #>#>#>#>#>#>#>#>#>#>*)
-	    @{thm solve_system4.simps})]
-\<close> ML \<open>
+
+method met_eqsys_topdown_4x4 : "EqSystem/top_down_substitution/4x4" =
+  \<open>{rew_ord'="ord_simplify_System", rls' = Rule_Set.Empty, calc = [], 
+    srls = Rule_Set.append_rules "srls_top_down_4x4" srls [], 
+    prls = Rule_Set.append_rules "prls_tri_4x4_lin_sys" prls_triangular
+        [\<^rule_eval>\<open>Prog_Expr.occurs_in\<close> (Prog_Expr.eval_occurs_in "")], 
+    crls = Rule_Set.Empty, errpats = [], nrls = Rule_Set.Empty}\<close>
+  (*FIXXXXME.WN060916: this script works ONLY for exp 7.79 #>#>#>#>#>#>#>#>#>#>*)
+  Program: solve_system4.simps
+  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))"
+    "(NTH 2 (v_s::real list)) occurs_in (NTH 2 (e_s::bool list))"
+    "(NTH 3 (v_s::real list)) occurs_in (NTH 3 (e_s::bool list))"
+    "(NTH 4 (v_s::real list)) occurs_in (NTH 4 (e_s::bool list))"
+  Find: "solution ss'''"
+
+ML \<open>
 \<close> ML \<open>
 \<close> ML \<open>
 \<close>