1.1 --- a/test/Tools/isac/Specify/refine.thy Wed May 13 12:14:49 2020 +0200
1.2 +++ b/test/Tools/isac/Specify/refine.thy Wed May 13 16:10:22 2020 +0200
1.3 @@ -14,30 +14,30 @@
1.4
1.5 section \<open>data for test "-ptyps.thy: store test-pbtyps by 'setup' ---"\<close>
1.6 setup \<open>KEStore_Elems.add_pbts
1.7 -[(Specify.prep_pbt thy "pbl_test_refine" [] Problem.id_empty
1.8 +[(Problem.prep_input thy "pbl_test_refine" [] Problem.id_empty
1.9 (["refine", "test"], [], Rule_Set.empty, NONE, [])),
1.10 -(Specify.prep_pbt @{theory DiffApp} "pbl_pbla" [] Problem.id_empty
1.11 +(Problem.prep_input @{theory DiffApp} "pbl_pbla" [] Problem.id_empty
1.12 (["pbla", "refine", "test"],
1.13 [("#Given", ["fixedValues a_a"])], Rule_Set.empty, NONE, [])),
1.14 -(Specify.prep_pbt @{theory DiffApp} "pbl_pbla1" [] Problem.id_empty
1.15 +(Problem.prep_input @{theory DiffApp} "pbl_pbla1" [] Problem.id_empty
1.16 (["pbla1","pbla", "refine", "test"],
1.17 [("#Given", ["fixedValues a_a","maximum a_1"])], Rule_Set.empty, NONE, [])),
1.18 -(Specify.prep_pbt @{theory DiffApp} "pbl_pbla2" [] Problem.id_empty
1.19 +(Problem.prep_input @{theory DiffApp} "pbl_pbla2" [] Problem.id_empty
1.20 (["pbla2","pbla", "refine", "test"],
1.21 [("#Given", ["fixedValues a_a","valuesFor a_2"])], Rule_Set.empty, NONE, [])),
1.22 -(Specify.prep_pbt @{theory DiffApp} "pbl_pbla2x" [] Problem.id_empty
1.23 +(Problem.prep_input @{theory DiffApp} "pbl_pbla2x" [] Problem.id_empty
1.24 (["pbla2x","pbla2","pbla", "refine", "test"],
1.25 [("#Given", ["fixedValues a_a","valuesFor a_2","functionOf a2_x"])],
1.26 Rule_Set.empty, NONE, [])),
1.27 -(Specify.prep_pbt @{theory DiffApp} "pbl_pbla2y" [] Problem.id_empty
1.28 +(Problem.prep_input @{theory DiffApp} "pbl_pbla2y" [] Problem.id_empty
1.29 (["pbla2y","pbla2","pbla", "refine", "test"],
1.30 [("#Given" ,["fixedValues a_a","valuesFor a_2","boundVariable a2_y"])],
1.31 Rule_Set.empty, NONE, [])),
1.32 -(Specify.prep_pbt @{theory DiffApp} "pbl_pbla2z" [] Problem.id_empty
1.33 +(Problem.prep_input @{theory DiffApp} "pbl_pbla2z" [] Problem.id_empty
1.34 (["pbla2z","pbla2","pbla", "refine", "test"],
1.35 [("#Given" ,["fixedValues a_a","valuesFor a_2","interval a2_z"])],
1.36 Rule_Set.empty, NONE, [])),
1.37 -(Specify.prep_pbt @{theory DiffApp} "pbl_pbla3" [] Problem.id_empty
1.38 +(Problem.prep_input @{theory DiffApp} "pbl_pbla3" [] Problem.id_empty
1.39 (["pbla3","pbla", "refine", "test"],
1.40 [("#Given" ,["fixedValues a_a","relations a_3"])],
1.41 Rule_Set.empty, NONE, []))]