1.1 --- a/src/Tools/isac/Knowledge/Test.thy	Fri Nov 30 12:27:18 2018 +0100
     1.2 +++ b/src/Tools/isac/Knowledge/Test.thy	Fri Nov 30 15:00:01 2018 +0100
     1.3 @@ -947,8 +947,29 @@
     1.4            "  L_L = Tac solve_equation_dummy                             " ^
     1.5            "  in Check_elementwise L_L {(v_v::real). Assumptions})")]
     1.6  \<close>
     1.7 -partial_function (tailrec) dummy4 :: "real \<Rightarrow> real"
     1.8 -  where "dummy4 xxx = xxx"
     1.9 +
    1.10 +partial_function (tailrec) solve_root_equation ::
    1.11 +  "bool \<Rightarrow> real \<Rightarrow> bool list"
    1.12 +where "minisubpbl e_e v_v =
    1.13 +  (let e_e = ((Try (Rewrite_Set ''norm_equation'' False)) @@
    1.14 +              (Try (Rewrite_Set ''Test_simplify'' False))) e_e;
    1.15 +      (L_L::bool list) =
    1.16 +             (SubProblem (''TestX'',
    1.17 +                 [''LINEAR'', ''univariate'', ''equation'', ''test''],
    1.18 +                 [''Test'', ''solve_linear''])
    1.19 +               [BOOL e_e, REAL v_v])
    1.20 +   in Check_elementwise L_L {(v_v::real). Assumptions})"
    1.21 +
    1.22 +(* ^^^used for test/../Minisubpbl/
    1.23 +# difference between partial_function above and Script below:
    1.24 +"Solve_root_equation" is a constant, which is NOT accepted by partial_function
    1.25 +
    1.26 +# differences between original "Solve_root_equation" and the version below:
    1.27 +(1) the program name, see note above
    1.28 +(2) the first argument of SubProblem: ''Test''' is NOT accepted by partial_function,
    1.29 +    thus previous change-set Test' \<longrightarrow> TestX
    1.30 +''Test'#TODO#''. Note: this change is NOT recognised by Interpret!
    1.31 +*)
    1.32  setup \<open>KEStore_Elems.add_mets
    1.33      [Specify.prep_met thy "met_test_squ_sub" [] Celem.e_metID
    1.34        (*tests subproblem fixed linear*)
    1.35 @@ -960,15 +981,15 @@
    1.36            prls = Rule.append_rls "prls_met_test_squ_sub" Rule.e_rls
    1.37                [Rule.Calc ("Test.precond'_rootmet", eval_precond_rootmet "")],
    1.38            calc=[], crls=tval_rls, errpats = [], nrls = Test_simplify},
    1.39 -        "Script Solve_root_equation (e_e::bool) (v_v::real) =       " ^
    1.40 -        " (let e_e = ((Try (Rewrite_Set norm_equation False)) @@    " ^
    1.41 -        "            (Try (Rewrite_Set Test_simplify False))) e_e;  " ^
    1.42 -        "     (L_L::bool list) =                                    " ^
    1.43 -        "            (SubProblem (TestX,                            " ^
    1.44 -        "                         [LINEAR,univariate,equation,test]," ^
    1.45 -        "                         [Test,solve_linear])              " ^
    1.46 -        "                        [BOOL e_e, REAL v_v])              " ^
    1.47 -        "  in Check_elementwise L_L {(v_v::real). Assumptions})     ")]
    1.48 +        "Script Solve_root_equation (e_e::bool) (v_v::real) =                  " ^
    1.49 +        " (let e_e = ((Try (Rewrite_Set norm_equation False)) @@               " ^
    1.50 +        "             (Try (Rewrite_Set Test_simplify False))) e_e;            " ^
    1.51 +        "     (L_L::bool list) =                                               " ^
    1.52 +        "            (SubProblem (''TestX'',                                   " ^
    1.53 +        "                [''LINEAR'', ''univariate'', ''equation'', ''test''], " ^
    1.54 +        "                [''Test'', ''solve_linear''])                         " ^
    1.55 +        "              [BOOL e_e, REAL v_v])                                   " ^
    1.56 +        "  in Check_elementwise L_L {(v_v::real). Assumptions})                ")]
    1.57  \<close>
    1.58  partial_function (tailrec) dummy7 :: "real \<Rightarrow> real"
    1.59    where "dummy7 xxx = xxx"