test/Tools/isac/Specify/refine.thy
changeset 59973 8a46c2e7c27a
parent 59967 f83918acd7d7
child 59997 46fe5a8c3911
     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, []))]