diff -r dbe1a10234df -r 4035ec339062 src/Tools/isac/Knowledge/EqSystem.thy
--- a/src/Tools/isac/Knowledge/EqSystem.thy	Tue May 28 16:52:30 2019 +0200
+++ b/src/Tools/isac/Knowledge/EqSystem.thy	Wed May 29 10:36:16 2019 +0200
@@ -520,14 +520,14 @@
 	    (["EqSystem"], [],
 	      {rew_ord'="tless_true", rls' = Rule.Erls, calc = [], srls = Rule.Erls, prls = Rule.Erls, crls = Rule.Erls,
           errpats = [], nrls = Rule.Erls},
-	      "empty_script"),
+	      @{thm refl}),
     Specify.prep_met thy "met_eqsys_topdown" [] Celem.e_metID
       (["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")]
+       @{thm refl})]
 \<close>
-(*ok
+
 partial_function (tailrec) solve_system :: "bool list => real list => bool list"
   where
 "solve_system e_s v_s =                          
@@ -546,7 +546,6 @@
                                   ''simplify_System'' False))) e_2;                 
        e__s = Take [e_1, e_2]                                                       
    in Try (Rewrite_Set ''order_system'' False) e__s)                              "
-*)
 setup \<open>KEStore_Elems.add_mets
     [Specify.prep_met thy "met_eqsys_topdown_2x2" [] Celem.e_metID
       (["EqSystem", "top_down_substitution", "2x2"],
@@ -561,7 +560,8 @@
 				        Rule.Thm ("tl_Cons",TermC.num_str @{thm tl_Cons}),
 				        Rule.Thm ("tl_Nil",TermC.num_str @{thm tl_Nil})], 
 	        prls = prls_triangular, crls = Rule.Erls, errpats = [], nrls = Rule.Erls},
-	      "Script SolveSystemScript (e_s::bool list) (v_s::real list) =                " ^
+	      @{thm solve_system.simps}
+	    (*"Script SolveSystemScript (e_s::bool list) (v_s::real list) =                " ^
           "  (let e_1 = Take (hd e_s);                                                " ^
           "       e_1 = ((Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s),(''bdv_2'', hd (tl v_s))]" ^
           "                                  ''isolate_bdvs'' False))     @@               " ^
@@ -576,7 +576,7 @@
           "               (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s),(''bdv_2'', hd (tl v_s))]" ^
           "                                  ''simplify_System'' False))) e_2;            " ^
           "       e__s = Take [e_1, e_2]                                             " ^
-          "   in (Try (Rewrite_Set ''order_system'' False)) e__s)"
+          "   in (Try (Rewrite_Set ''order_system'' False)) e__s)"*)
           (*---------------------------------------------------------------------------
             this script does NOT separate the equations as above, 
             but it does not yet work due to preliminary script-interpreter,
@@ -600,12 +600,12 @@
 	    (["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")]
+	      @{thm refl})]
 \<close>
-(*ok
+
 partial_function (tailrec) solve_system2 :: "bool list => real list => bool list"
   where
-"solve_system e_s v_s =
+"solve_system2 e_s v_s =
   (let e__s = ((Try (Rewrite_Set ''norm_Rational'' False)) @@
                (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s), (''bdv_2'', hd (tl v_s))]
                                   ''simplify_System_parenthesized'' False)) @@
@@ -616,7 +616,6 @@
                (Try (Rewrite_Set ''order_system'' False))) e_s
    in (SubProblem (''EqSystem'', [''LINEAR'', ''system''], [''no_met''])
                   [BOOL_LIST e__s, REAL_LIST v_s]))"
-*)
 setup \<open>KEStore_Elems.add_mets
     [Specify.prep_met thy "met_eqsys_norm_2x2" [] Celem.e_metID
 	    (["EqSystem","normalise","2x2"],
@@ -628,7 +627,8 @@
 				        Rule.Thm ("tl_Cons",TermC.num_str @{thm tl_Cons}),
 				        Rule.Thm ("tl_Nil",TermC.num_str @{thm tl_Nil})], 
 		      prls = Rule.Erls, crls = Rule.Erls, errpats = [], nrls = Rule.Erls},
-		    "Script SolveSystemScript (e_s::bool list) (v_s::real list) =                " ^
+		    @{thm solve_system2.simps}
+	    (*"Script SolveSystemScript (e_s::bool list) (v_s::real list) =                " ^
           "  (let e__s = ((Try (Rewrite_Set ''norm_Rational'' False)) @@                   " ^
           "               (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s),(''bdv_2'', hd (tl v_s))]" ^
           "                                  ''simplify_System_parenthesized'' False)) @@  " ^
@@ -638,12 +638,12 @@
           "                                  ''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]))")]
+          "                  [BOOL_LIST e__s, REAL_LIST v_s]))"*))]
 \<close>
-(*ok
+
 partial_function (tailrec) solve_system3 :: "bool list => real list => bool list"
   where
-"solve_system e_s v_s =
+"solve_system3 e_s v_s =
   (let e__s =
      ((Try (Rewrite_Set ''norm_Rational'' False)) @@
       (Repeat (Rewrite ''commute_0_equality'' False)) @@
@@ -659,7 +659,6 @@
       (Try (Rewrite_Set ''order_system'' False)))  e_s
    in (SubProblem (''EqSystem'', [''LINEAR'', ''system''], [''no_met''])
                   [BOOL_LIST e__s, REAL_LIST v_s]))"
-*)
 setup \<open>KEStore_Elems.add_mets
     [Specify.prep_met thy "met_eqsys_norm_4x4" [] Celem.e_metID
 	      (["EqSystem","normalise","4x4"],
@@ -672,7 +671,8 @@
 	               Rule.Thm ("tl_Nil",TermC.num_str @{thm tl_Nil})], 
 		       prls = Rule.Erls, crls = Rule.Erls, errpats = [], nrls = Rule.Erls},
 		     (*STOPPED.WN06? met ["EqSystem","normalise","4x4"] @@@@@@@@@@@@@@@@@@@@@@@@@@@*)
-		     "Script SolveSystemScript (e_s::bool list) (v_s::real list) =                " ^
+		     @{thm solve_system3.simps}
+	    (*""Script SolveSystemScript (e_s::bool list) (v_s::real list) =                " ^
            "  (let e__s =                                                               " ^
            "     ((Try (Rewrite_Set ''norm_Rational'' False)) @@                            " ^
            "      (Repeat (Rewrite ''commute_0_equality'' False)) @@                        " ^
@@ -687,12 +687,12 @@
            "                             ''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]))")]
+           "                  [BOOL_LIST e__s, REAL_LIST v_s]))"*))]
 \<close>
-(*ok
+
 partial_function (tailrec) solve_system4 :: "bool list => real list => bool list"
   where
-"solve_system e_s v_s =
+"solve_system4 e_s v_s =
   (let e_1 = NTH 1 e_s;
        e_2 = Take (NTH 2 e_s);
        e_2 = ((Substitute [e_1]) @@
@@ -706,7 +706,6 @@
                                       (''bdv_3'',NTH 3 v_s),(''bdv_4'',NTH 4 v_s)]
                                  ''norm_Rational'' False))) e_2
     in [e_1, e_2, NTH 3 e_s, NTH 4 e_s])"
-*)
 setup \<open>KEStore_Elems.add_mets
     [Specify.prep_met thy "met_eqsys_topdown_4x4" [] Celem.e_metID
 	    (["EqSystem","top_down_substitution","4x4"],
@@ -723,7 +722,8 @@
 			      [Rule.Calc ("Atools.occurs'_in",eval_occurs_in "")], 
 	      crls = Rule.Erls, errpats = [], nrls = Rule.Erls},
 	    (*FIXXXXME.WN060916: this script works ONLY for exp 7.79 @@@@@@@@@@@@@@@@@@@@*)
-	    "Script SolveSystemScript (e_s::bool list) (v_s::real list) =                " ^
+	    @{thm solve_system4.simps}
+	    (*"Script SolveSystemScript (e_s::bool list) (v_s::real list) =                " ^
         "  (let e_1 = NTH 1 e_s;                                                    " ^
         "       e_2 = Take (NTH 2 e_s);                                             " ^
         "       e_2 = ((Substitute [e_1]) @@                                         " ^
@@ -736,7 +736,7 @@
         "              (Try (Rewrite_Set_Inst [(''bdv_1'',NTH 1 v_s),(''bdv_2'',NTH 2 v_s)," ^
         "                                      (''bdv_3'',NTH 3 v_s),(''bdv_4'',NTH 4 v_s)]" ^
         "                                 ''norm_Rational'' False)))             e_2     " ^
-        "    in [e_1, e_2, NTH 3 e_s, NTH 4 e_s])")]
+        "    in [e_1, e_2, NTH 3 e_s, NTH 4 e_s])"*))]
 \<close>
 
 end
\ No newline at end of file