equal
deleted
inserted
replaced
892 | NONE => error "check_error_patterns broken"; |
892 | NONE => error "check_error_patterns broken"; |
893 |
893 |
894 |
894 |
895 "--------- embed fun check_error_patterns ------------------------"; |
895 "--------- embed fun check_error_patterns ------------------------"; |
896 "--------- embed fun check_error_patterns ------------------------"; |
896 "--------- embed fun check_error_patterns ------------------------"; |
|
897 (*========== inhibit exn WN1130621 Isabelle2012-->13 !thehier! ==================== |
897 "--------- embed fun check_error_patterns ------------------------"; |
898 "--------- embed fun check_error_patterns ------------------------"; |
898 states:=[]; |
899 states:=[]; |
899 CalcTree |
900 CalcTree |
900 [(["functionTerm (x ^ 2 + sin (x ^ 4))", "differentiateFor x", "derivative f_f'"], |
901 [(["functionTerm (x ^ 2 + sin (x ^ 4))", "differentiateFor x", "derivative f_f'"], |
901 ("Isac", ["derivative_of","function"], ["diff","differentiate_on_R"]))]; |
902 ("Isac", ["derivative_of","function"], ["diff","differentiate_on_R"]))]; |
1114 val (Form f, _, asms) = pt_extract (pt, p); |
1115 val (Form f, _, asms) = pt_extract (pt, p); |
1115 if p = ([2], Res) andalso |
1116 if p = ([2], Res) andalso |
1116 term2str f = "d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x (x ^^^ 4)" andalso |
1117 term2str f = "d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x (x ^^^ 4)" andalso |
1117 get_obj g_tac pt (fst p) = Rewrite_Inst (["(bdv, x)"], ("diff_sin_chain", "")) |
1118 get_obj g_tac pt (fst p) = Rewrite_Inst (["(bdv, x)"], ("diff_sin_chain", "")) |
1118 then () else error "inputFillFormula changed 11"; |
1119 then () else error "inputFillFormula changed 11"; |
1119 |
1120 ============ inhibit exn WN1130621 Isabelle2012-->13 !thehier! ==================*) |
|
1121 |