14 "----------- retrieve errpats ------------------------------------"; |
14 "----------- retrieve errpats ------------------------------------"; |
15 "----------- fun collect_part: KILL BY [[ML_print_depth = 999]]---"; |
15 "----------- fun collect_part: KILL BY [[ML_print_depth = 999]]---"; |
16 "-----------------------------------------------------------------"; |
16 "-----------------------------------------------------------------"; |
17 "-----------------------------------------------------------------"; |
17 "-----------------------------------------------------------------"; |
18 "-----------------------------------------------------------------"; |
18 "-----------------------------------------------------------------"; |
|
19 val thy = @{theory Build_Thydata} |
|
20 val ctxt = Proof_Context.init_global thy; |
19 |
21 |
20 "----------- retrieve errpats ------------------------------------"; |
22 "----------- retrieve errpats ------------------------------------"; |
21 "----------- retrieve errpats ------------------------------------"; |
23 "----------- retrieve errpats ------------------------------------"; |
22 "----------- retrieve errpats ------------------------------------"; |
24 "----------- retrieve errpats ------------------------------------"; |
23 val {errpats, rew_rls, program = Prog prog, ...} = MethodC.from_store ctxt ["diff", "differentiate_on_R"]; |
25 val {errpats, rew_rls, program = Prog prog, ...} = |
|
26 MethodC.from_store ctxt ["diff", "differentiate_on_R"]; |
24 case errpats of [("chain-rule-diff-both", _, _)] => () |
27 case errpats of [("chain-rule-diff-both", _, _)] => () |
25 | _ => error "errpats chain-rule-diff-both changed" |
28 | _ => error "errpats chain-rule-diff-both changed" |
26 |
29 |
27 "----------- fun collect_part: KILL BY [[ML_print_depth = 999]]---"; |
30 "----------- fun collect_part: KILL BY [[ML_print_depth = 999]]---"; |
28 "----------- fun collect_part: KILL BY [[ML_print_depth = 999]]---"; |
31 "----------- fun collect_part: KILL BY [[ML_print_depth = 999]]---"; |