1.1 --- a/test/Tools/isac/Test_Isac.thy	Mon Jan 27 13:40:36 2014 +0100
     1.2 +++ b/test/Tools/isac/Test_Isac.thy	Mon Jan 27 21:49:27 2014 +0100
     1.3 @@ -45,20 +45,39 @@
     1.4    ML {*"%%%%%%%%%%%%%%%%% end Isabelle %%%%%%%%%%%%%%%%%%%%%%%%%";*}
     1.5  
     1.6  section {* test ML Code of isac *}
     1.7 +  setup {* KEStore_Elems.add_pbts
     1.8 +    [prep_pbt @{theory "Test"} "pbl_ttest" [] e_pblID (["test"], [], e_rls, NONE, []),
     1.9 +      prep_pbt @{theory "Test"} "pbl_ttest_calc" [] e_pblID
    1.10 +        (["calculate","test"],
    1.11 +          [("#Given" ,["realTestGiven t_t"]),
    1.12 +            ("#Find"  ,["realTestFind s_s"])],
    1.13 +          e_rls, NONE, [["Test","test_calculate"]]),
    1.14 +       prep_pbt thy "pbl_test_refine" [] e_pblID (["refine", "test"], [], e_rls, NONE, []),
    1.15 +       prep_pbt @{theory DiffApp} "pbl_pbla" [] e_pblID
    1.16 +         (["pbla", "refine", "test"], [("#Given", ["fixedValues a_a"])], e_rls, NONE, []),
    1.17 +       prep_pbt @{theory DiffApp} "pbl_pbla1" [] e_pblID
    1.18 +         (["pbla1","pbla", "refine", "test"],
    1.19 +           [("#Given", ["fixedValues a_a","maximum a_1"])], e_rls, NONE, []),
    1.20 +       prep_pbt @{theory DiffApp} "pbl_pbla2" [] e_pblID
    1.21 +         (["pbla2","pbla", "refine", "test"], 
    1.22 +           [("#Given", ["fixedValues a_a","valuesFor a_2"])], e_rls, NONE, []),
    1.23 +       prep_pbt @{theory DiffApp} "pbl_pbla2x" [] e_pblID
    1.24 +         (["pbla2x","pbla2","pbla", "refine", "test"],
    1.25 +           [("#Given", ["fixedValues a_a","valuesFor a_2","functionOf a2_x"])], e_rls, NONE, []),
    1.26 +       prep_pbt @{theory DiffApp} "pbl_pbla2y" [] e_pblID
    1.27 +         (["pbla2y","pbla2","pbla", "refine", "test"],
    1.28 +           [("#Given" ,["fixedValues a_a","valuesFor a_2","boundVariable a2_y"])], e_rls, NONE, []),
    1.29 +       prep_pbt @{theory DiffApp} "pbl_pbla2z" [] e_pblID
    1.30 +         (["pbla2z","pbla2","pbla", "refine", "test"],
    1.31 +           [("#Given" ,["fixedValues a_a","valuesFor a_2","interval a2_z"])], e_rls, NONE, []),
    1.32 +       prep_pbt @{theory DiffApp} "pbl_pbla3" [] e_pblID
    1.33 +         (["pbla3","pbla", "refine", "test"],
    1.34 +           [("#Given" ,["fixedValues a_a","relations a_3"])], e_rls, NONE, [])] *}
    1.35    ML {*"%%%%%%%%%%%%%%%%% start ProgLang.thy %%%%%%%%%%%%%%%%%%%";*}
    1.36    ML_file          "library.sml"
    1.37    ML_file          "calcelems.sml"
    1.38    ML_file          "kestore.sml"
    1.39    ML_file "ProgLang/termC.sml"
    1.40 -
    1.41 -  setup {* store_pbts
    1.42 -    [prep_pbt @{theory "Test"} "pbl_ttest" [] e_pblID (["test"], [], e_rls, NONE, []),
    1.43 -      prep_pbt @{theory "Test"} "pbl_ttest_calc" [] e_pblID
    1.44 -        (["calculate","test"],
    1.45 -          [("#Given" ,["realTestGiven t_t"]),
    1.46 -            ("#Find"  ,["realTestFind s_s"])],
    1.47 -          e_rls, NONE, [["Test","test_calculate"]])] *}
    1.48 -
    1.49    ML_file "ProgLang/calculate.sml"
    1.50    ML_file "ProgLang/rewrite.sml"
    1.51    ML_file "ProgLang/listC.sml"