1.1 --- a/src/Tools/isac/Knowledge/Build_Thydata.thy	Sat Oct 08 15:41:11 2022 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Build_Thydata.thy	Sat Oct 08 15:57:10 2022 +0200
     1.3 @@ -139,11 +139,11 @@
     1.4  setup \<open>KEStore_Elems.add_mets @{context}
     1.5    [Pbl_Met_Hierarchy.update_metpair_PIDE @{theory Diff} ["diff", "differentiate_on_R"]
     1.6        [("chain-rule-diff-both",
     1.7 -        [TermC.parse_patt @{theory Diff} "d_d ?bdv (sin ?u) = cos (d_d ?bdv ?u)",
     1.8 -         TermC.parse_patt @{theory Diff} "d_d ?bdv (cos ?u) = - sin (d_d ?bdv ?u)",
     1.9 -         TermC.parse_patt @{theory Diff} "d_d ?bdv (?u \<up> ?n) = ?n * ?u \<up> (?n - 1)",
    1.10 -         TermC.parse_patt @{theory Diff} "d_d ?bdv (LogExp.ln ?u) = 1 / ?u",
    1.11 -         TermC.parse_patt @{theory Diff} "d_d ?bdv (LogExp.ln ?u) = 1 / d_d ?bdv ?u"],
    1.12 +        [TermC.parse_patt_PIDE @{theory Diff} "d_d ?bdv (sin ?u) = cos (d_d ?bdv ?u)",
    1.13 +         TermC.parse_patt_PIDE @{theory Diff} "d_d ?bdv (cos ?u) = - sin (d_d ?bdv ?u)",
    1.14 +         TermC.parse_patt_PIDE @{theory Diff} "d_d ?bdv (?u \<up> ?n) = ?n * ?u \<up> (?n - 1)",
    1.15 +         TermC.parse_patt_PIDE @{theory Diff} "d_d ?bdv (LogExp.ln ?u) = 1 / ?u",
    1.16 +         TermC.parse_patt_PIDE @{theory Diff} "d_d ?bdv (LogExp.ln ?u) = 1 / d_d ?bdv ?u"],
    1.17          [@{thm diff_sin_chain}, @{thm diff_cos_chain}, @{thm diff_pow_chain}, @{thm diff_ln_chain},
    1.18            @{thm  diff_exp_chain}])]]
    1.19  \<close>
    1.20 @@ -169,11 +169,11 @@
    1.21  setup \<open>KEStore_Elems.add_mets @{context}
    1.22    [Pbl_Met_Hierarchy.update_metpair_PIDE @{theory Rational} ["simplification", "of_rationals"]
    1.23        [("addition-of-fractions",
    1.24 -        [TermC.parse_patt @{theory Rational} "(?a / ?b + ?c / ?d) = (?a + ?c)/(?b + ?d)",
    1.25 -         TermC.parse_patt @{theory Rational} "(?a / ?b + ?c / ?d) = (?a + ?c)/(?b * ?d)",
    1.26 -         TermC.parse_patt @{theory Rational} "(?a / ?b + ?c / ?d) = (?c * ?a)/(?d * ?b)",
    1.27 -         TermC.parse_patt @{theory Rational} "?a + (?b /?c)= (?a + ?b)/ ?c",
    1.28 -         TermC.parse_patt @{theory Rational} "?a + (?b /?c)= (?a * ?b)/ ?c"],
    1.29 +        [TermC.parse_patt_PIDE @{theory Rational} "(?a / ?b + ?c / ?d) = (?a + ?c)/(?b + ?d)",
    1.30 +         TermC.parse_patt_PIDE @{theory Rational} "(?a / ?b + ?c / ?d) = (?a + ?c)/(?b * ?d)",
    1.31 +         TermC.parse_patt_PIDE @{theory Rational} "(?a / ?b + ?c / ?d) = (?c * ?a)/(?d * ?b)",
    1.32 +         TermC.parse_patt_PIDE @{theory Rational} "?a + (?b /?c)= (?a + ?b)/ ?c",
    1.33 +         TermC.parse_patt_PIDE @{theory Rational} "?a + (?b /?c)= (?a * ?b)/ ?c"],
    1.34          [@{thm rat_add}, @{thm rat_add_assoc}, @{thm rat_add1}, @{thm rat_add1_assoc},
    1.35            @{thm rat_add2}, @{thm rat_add2_assoc}, @{thm rat_add3}, @{thm rat_add3_assoc}])]]
    1.36  \<close>

     2.1 Binary file test/Tools/isac/Frontend/.interface.sml.swp has changed