1.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy	Tue Feb 19 19:35:12 2019 +0100
     1.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy	Thu Feb 28 12:14:32 2019 +0100
     1.3 @@ -527,6 +527,7 @@
     1.4            errpats = [], nrls = Rule.Erls},
     1.5         "empty_script")]
     1.6  \<close>
     1.7 +(*ok
     1.8  partial_function (tailrec) solve_system :: "bool list => real list => bool list"
     1.9    where
    1.10  "solve_system e_s v_s =                          
    1.11 @@ -545,6 +546,7 @@
    1.12                                    ''simplify_System'' False))) e_2;                 
    1.13         e__s = Take [e_1, e_2]                                                       
    1.14     in Try (Rewrite_Set ''order_system'' False) e__s)                              "
    1.15 +*)
    1.16  setup \<open>KEStore_Elems.add_mets
    1.17      [Specify.prep_met thy "met_eqsys_topdown_2x2" [] Celem.e_metID
    1.18        (["EqSystem", "top_down_substitution", "2x2"],
    1.19 @@ -600,6 +602,7 @@
    1.20            errpats = [], nrls = Rule.Erls},
    1.21  	      "empty_script")]
    1.22  \<close>
    1.23 +(*ok
    1.24  partial_function (tailrec) solve_system2 :: "bool list => real list => bool list"
    1.25    where
    1.26  "solve_system e_s v_s =
    1.27 @@ -613,6 +616,7 @@
    1.28                 (Try (Rewrite_Set ''order_system'' False))) e_s
    1.29     in (SubProblem (''EqSystem'', [''LINEAR'', ''system''], [''no_met''])
    1.30                    [BOOL_LIST e__s, REAL_LIST v_s]))"
    1.31 +*)
    1.32  setup \<open>KEStore_Elems.add_mets
    1.33      [Specify.prep_met thy "met_eqsys_norm_2x2" [] Celem.e_metID
    1.34  	    (["EqSystem","normalise","2x2"],
    1.35 @@ -636,6 +640,7 @@
    1.36            "   in (SubProblem (''EqSystem'',[''LINEAR'',''system''],[''no_met''])                      " ^
    1.37            "                  [BOOL_LIST e__s, REAL_LIST v_s]))")]
    1.38  \<close>
    1.39 +(*ok
    1.40  partial_function (tailrec) solve_system3 :: "bool list => real list => bool list"
    1.41    where
    1.42  "solve_system e_s v_s =
    1.43 @@ -654,6 +659,7 @@
    1.44        (Try (Rewrite_Set ''order_system'' False)))  e_s
    1.45     in (SubProblem (''EqSystem'', [''LINEAR'', ''system''], [''no_met''])
    1.46                    [BOOL_LIST e__s, REAL_LIST v_s]))"
    1.47 +*)
    1.48  setup \<open>KEStore_Elems.add_mets
    1.49      [Specify.prep_met thy "met_eqsys_norm_4x4" [] Celem.e_metID
    1.50  	      (["EqSystem","normalise","4x4"],
    1.51 @@ -683,6 +689,7 @@
    1.52             "   in (SubProblem (''EqSystem'',[''LINEAR'',''system''],[''no_met''])                      " ^
    1.53             "                  [BOOL_LIST e__s, REAL_LIST v_s]))")]
    1.54  \<close>
    1.55 +(*ok
    1.56  partial_function (tailrec) solve_system4 :: "bool list => real list => bool list"
    1.57    where
    1.58  "solve_system e_s v_s =
    1.59 @@ -699,6 +706,7 @@
    1.60                                        (''bdv_3'',NTH 3 v_s),(''bdv_4'',NTH 4 v_s)]
    1.61                                   ''norm_Rational'' False))) e_2
    1.62      in [e_1, e_2, NTH 3 e_s, NTH 4 e_s])"
    1.63 +*)
    1.64  setup \<open>KEStore_Elems.add_mets
    1.65      [Specify.prep_met thy "met_eqsys_topdown_4x4" [] Celem.e_metID
    1.66  	    (["EqSystem","top_down_substitution","4x4"],