14 |
14 |
15 section \<open>data for test "-ptyps.thy: store test-pbtyps by 'setup' ---"\<close> |
15 section \<open>data for test "-ptyps.thy: store test-pbtyps by 'setup' ---"\<close> |
16 setup \<open>KEStore_Elems.add_pbts |
16 setup \<open>KEStore_Elems.add_pbts |
17 [(Problem.prep_input @{theory} "pbl_test_refine" [] Problem.id_empty |
17 [(Problem.prep_input @{theory} "pbl_test_refine" [] Problem.id_empty |
18 (["refine", "test"], [], Rule_Set.empty, NONE, [])), |
18 (["refine", "test"], [], Rule_Set.empty, NONE, [])), |
19 (Problem.prep_input @{theory DiffApp} "pbl_pbla" [] Problem.id_empty |
19 (Problem.prep_input @{theory Diff_App} "pbl_pbla" [] Problem.id_empty |
20 (["pbla", "refine", "test"], |
20 (["pbla", "refine", "test"], |
21 [("#Given", ["fixedValues a_a"])], Rule_Set.empty, NONE, [])), |
21 [("#Given", ["fixedValues a_a"])], Rule_Set.empty, NONE, [])), |
22 (Problem.prep_input @{theory DiffApp} "pbl_pbla1" [] Problem.id_empty |
22 (Problem.prep_input @{theory Diff_App} "pbl_pbla1" [] Problem.id_empty |
23 (["pbla1", "pbla", "refine", "test"], |
23 (["pbla1", "pbla", "refine", "test"], |
24 [("#Given", ["fixedValues a_a", "maximum a_1"])], Rule_Set.empty, NONE, [])), |
24 [("#Given", ["fixedValues a_a", "maximum a_1"])], Rule_Set.empty, NONE, [])), |
25 (Problem.prep_input @{theory DiffApp} "pbl_pbla2" [] Problem.id_empty |
25 (Problem.prep_input @{theory Diff_App} "pbl_pbla2" [] Problem.id_empty |
26 (["pbla2", "pbla", "refine", "test"], |
26 (["pbla2", "pbla", "refine", "test"], |
27 [("#Given", ["fixedValues a_a", "valuesFor a_2"])], Rule_Set.empty, NONE, [])), |
27 [("#Given", ["fixedValues a_a", "valuesFor a_2"])], Rule_Set.empty, NONE, [])), |
28 (Problem.prep_input @{theory DiffApp} "pbl_pbla2x" [] Problem.id_empty |
28 (Problem.prep_input @{theory Diff_App} "pbl_pbla2x" [] Problem.id_empty |
29 (["pbla2x", "pbla2", "pbla", "refine", "test"], |
29 (["pbla2x", "pbla2", "pbla", "refine", "test"], |
30 [("#Given", ["fixedValues a_a", "valuesFor a_2", "functionOf a2_x"])], |
30 [("#Given", ["fixedValues a_a", "valuesFor a_2", "functionOf a2_x"])], |
31 Rule_Set.empty, NONE, [])), |
31 Rule_Set.empty, NONE, [])), |
32 (Problem.prep_input @{theory DiffApp} "pbl_pbla2y" [] Problem.id_empty |
32 (Problem.prep_input @{theory Diff_App} "pbl_pbla2y" [] Problem.id_empty |
33 (["pbla2y", "pbla2", "pbla", "refine", "test"], |
33 (["pbla2y", "pbla2", "pbla", "refine", "test"], |
34 [("#Given" ,["fixedValues a_a", "valuesFor a_2", "boundVariable a2_y"])], |
34 [("#Given" ,["fixedValues a_a", "valuesFor a_2", "boundVariable a2_y"])], |
35 Rule_Set.empty, NONE, [])), |
35 Rule_Set.empty, NONE, [])), |
36 (Problem.prep_input @{theory DiffApp} "pbl_pbla2z" [] Problem.id_empty |
36 (Problem.prep_input @{theory Diff_App} "pbl_pbla2z" [] Problem.id_empty |
37 (["pbla2z", "pbla2", "pbla", "refine", "test"], |
37 (["pbla2z", "pbla2", "pbla", "refine", "test"], |
38 [("#Given" ,["fixedValues a_a", "valuesFor a_2", "interval a2_z"])], |
38 [("#Given" ,["fixedValues a_a", "valuesFor a_2", "interval a2_z"])], |
39 Rule_Set.empty, NONE, [])), |
39 Rule_Set.empty, NONE, [])), |
40 (Problem.prep_input @{theory DiffApp} "pbl_pbla3" [] Problem.id_empty |
40 (Problem.prep_input @{theory Diff_App} "pbl_pbla3" [] Problem.id_empty |
41 (["pbla3", "pbla", "refine", "test"], |
41 (["pbla3", "pbla", "refine", "test"], |
42 [("#Given" ,["fixedValues a_a", "relations a_3"])], |
42 [("#Given" ,["fixedValues a_a", "relations a_3"])], |
43 Rule_Set.empty, NONE, []))] |
43 Rule_Set.empty, NONE, []))] |
44 \<close> |
44 \<close> |
45 |
45 |