1.1 --- a/src/Tools/isac/Knowledge/Partial_Fractions.thy	Tue May 28 16:52:30 2019 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Partial_Fractions.thy	Wed May 29 10:36:16 2019 +0200
     1.3 @@ -192,7 +192,6 @@
     1.4  \<close>
     1.5  
     1.6  (* current version, error outcommented *)
     1.7 -(*ok
     1.8  partial_function (tailrec) partial_fraction :: "real \<Rightarrow> real \<Rightarrow> real"
     1.9    where
    1.10  "partial_fraction f_f zzz =              \<comment> \<open>([1], Frm), 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))\<close>
    1.11 @@ -232,7 +231,6 @@
    1.12    pbz = Take eqr;                            \<comment> \<open>([11], Res), 4 / (z - 1 / 2) + -4 / (z - -1 / 4)\<close>
    1.13    pbz = Substitute [AA = a, BB = b] pbz        \<comment> \<open>([], Res), 4 / (z - 1 / 2) + -4 / (z - -1 / 4)\<close>
    1.14  in pbz)                                                                                "
    1.15 -*)
    1.16  setup \<open>KEStore_Elems.add_mets
    1.17      [Specify.prep_met @{theory} "met_partial_fraction" [] Celem.e_metID
    1.18        (["simplification","of_rationals","to_partial_fraction"], 
    1.19 @@ -244,7 +242,8 @@
    1.20          {rew_ord'="tless_true", rls'= Rule.e_rls, calc = [], srls = srls_partial_fraction, prls = Rule.e_rls,
    1.21            crls = Rule.e_rls, errpats = [], nrls = Rule.e_rls},
    1.22          (*([], Frm), Problem (Partial_Fractions, [partial_fraction, rational, simplification])*)
    1.23 -        "Script PartFracScript (f_f::real) (zzz::real) =   " ^
    1.24 +        @{thm partial_fraction.simps}
    1.25 +	    (*"Script PartFracScript (f_f::real) (zzz::real) =   " ^
    1.26            (*([1], Frm), 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*)
    1.27            "(let f_f = Take f_f;                              " ^
    1.28            (*           num_orig = 3*)
    1.29 @@ -309,7 +308,7 @@
    1.30            (*([11], Res), 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*)
    1.31            "  pbz = ((Substitute [AA = a, BB = b]) pbz)         " ^
    1.32            (*([], Res), 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*)
    1.33 -          "in pbz)"
    1.34 +          "in pbz)"*)
    1.35  )]
    1.36  \<close>
    1.37  ML \<open>