1.1 --- a/src/Tools/isac/Knowledge/Build_Thydata.thy	Thu Aug 02 18:39:06 2012 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Build_Thydata.thy	Fri Aug 03 15:44:39 2012 +0200
     1.3 @@ -117,20 +117,18 @@
     1.4  
     1.5  (* interface for dialog-authoring *)
     1.6  
     1.7 -val errpats =
     1.8 -  [("chain-rule-diff-both",
     1.9 +insert_errpats ["diff","differentiate_on_R"]
    1.10 + ([("chain-rule-diff-both",
    1.11      [parse_patt @{theory} "d_d ?bdv (sin ?u) = cos (d_d ?bdv ?u)",
    1.12       parse_patt @{theory} "d_d ?bdv (cos ?u) = - sin (d_d ?bdv ?u)",
    1.13       parse_patt @{theory} "d_d ?bdv (?u ^^^ ?n) = ?n * ?u ^^^ (?n - 1)",
    1.14       parse_patt @{theory} "d_d ?bdv (LogExp.ln ?u) = 1 / ?u",
    1.15       parse_patt @{theory} "d_d ?bdv (LogExp.ln ?u) = 1 / d_d ?bdv ?u"],
    1.16      [@{thm diff_sin_chain}, @{thm diff_cos_chain}, @{thm diff_pow_chain}, 
    1.17 -     @{thm diff_ln_chain}, @{thm  diff_exp_chain}])];
    1.18 +     @{thm diff_ln_chain}, @{thm  diff_exp_chain}])]: errpat list);
    1.19  
    1.20 -insert_errpats ["diff","differentiate_on_R"] errpats;
    1.21 -
    1.22 -val fillpats = [
    1.23 -  ("fill-d_d-arg",
    1.24 +insert_fillpats ["IsacKnowledge", "Diff", "Theorems", "diff_sin_chain"]
    1.25 + ([("fill-d_d-arg",
    1.26      parse_patt @{theory Diff} "d_d ?bdv (sin ?u) = cos ?u * d_d ?bdv _", "chain-rule-diff-both"),
    1.27    ("fill-both-args",
    1.28      parse_patt @{theory Diff} "d_d ?bdv (sin ?u) = cos _ * d_d ?bdv _", "chain-rule-diff-both"),
    1.29 @@ -139,9 +137,7 @@
    1.30    ("fill-inner-deriv",
    1.31      parse_patt @{theory Diff} "d_d ?bdv (sin ?u) = cos ?u * _", "chain-rule-diff-both"),
    1.32    ("fill-all",
    1.33 -    parse_patt @{theory Diff} "d_d ?bdv (sin ?u) = _", "chain-rule-diff-both")]: fillpat list;
    1.34 -
    1.35 -insert_fillpats ["IsacKnowledge", "Diff", "Theorems", "diff_sin_chain"] fillpats;
    1.36 +    parse_patt @{theory Diff} "d_d ?bdv (sin ?u) = _", "chain-rule-diff-both")]: fillpat list);
    1.37  
    1.38  (*
    1.39  val fillpats = [
    1.40 @@ -188,8 +184,8 @@
    1.41  
    1.42  (* still ununsed; planned for stepToErrorpattern: this is just a reminder... *)
    1.43  
    1.44 -val errpattIDs = ["chain-rule-diff-both", "cancel"];
    1.45 -insert_errpatIDs ["IsacKnowledge", "Diff", "Rulesets", "norm_diff"] errpattIDs;
    1.46 +insert_errpatIDs ["IsacKnowledge", "Diff", "Rulesets", "norm_diff"]
    1.47 +  (["chain-rule-diff-both", "cancel"]: errpatID list);
    1.48  
    1.49  (* ...and all other related rls by hand;
    1.50     TODO: lift errpattIDs from theorems to respective rls AUTOMATICALLY *)