1.1 --- a/src/Tools/isac/Knowledge/Build_Thydata.thy	Mon Apr 19 20:44:18 2021 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Build_Thydata.thy	Tue Apr 20 16:58:44 2021 +0200
     1.3 @@ -119,7 +119,7 @@
     1.4        [("chain-rule-diff-both",
     1.5          [TermC.parse_patt @{theory Diff} "d_d ?bdv (sin ?u) = cos (d_d ?bdv ?u)",
     1.6           TermC.parse_patt @{theory Diff} "d_d ?bdv (cos ?u) = - sin (d_d ?bdv ?u)",
     1.7 -         TermC.parse_patt @{theory Diff} "d_d ?bdv (?u ^^^ ?n) = ?n * ?u ^^^ (?n - 1)",
     1.8 +         TermC.parse_patt @{theory Diff} "d_d ?bdv (?u \<up> ?n) = ?n * ?u \<up> (?n - 1)",
     1.9           TermC.parse_patt @{theory Diff} "d_d ?bdv (LogExp.ln ?u) = 1 / ?u",
    1.10           TermC.parse_patt @{theory Diff} "d_d ?bdv (LogExp.ln ?u) = 1 / d_d ?bdv ?u"],
    1.11          [@{thm diff_sin_chain}, @{thm diff_cos_chain}, @{thm diff_pow_chain}, @{thm diff_ln_chain},