43 ML_file "~~/test/Pure/General/basics.ML" |
43 ML_file "~~/test/Pure/General/basics.ML" |
44 ML_file "~~/test/Pure/General/scan.ML" |
44 ML_file "~~/test/Pure/General/scan.ML" |
45 ML {*"%%%%%%%%%%%%%%%%% end Isabelle %%%%%%%%%%%%%%%%%%%%%%%%%";*} |
45 ML {*"%%%%%%%%%%%%%%%%% end Isabelle %%%%%%%%%%%%%%%%%%%%%%%%%";*} |
46 |
46 |
47 section {* test ML Code of isac *} |
47 section {* test ML Code of isac *} |
|
48 setup {* KEStore_Elems.add_pbts |
|
49 [prep_pbt @{theory "Test"} "pbl_ttest" [] e_pblID (["test"], [], e_rls, NONE, []), |
|
50 prep_pbt @{theory "Test"} "pbl_ttest_calc" [] e_pblID |
|
51 (["calculate","test"], |
|
52 [("#Given" ,["realTestGiven t_t"]), |
|
53 ("#Find" ,["realTestFind s_s"])], |
|
54 e_rls, NONE, [["Test","test_calculate"]]), |
|
55 prep_pbt thy "pbl_test_refine" [] e_pblID (["refine", "test"], [], e_rls, NONE, []), |
|
56 prep_pbt @{theory DiffApp} "pbl_pbla" [] e_pblID |
|
57 (["pbla", "refine", "test"], [("#Given", ["fixedValues a_a"])], e_rls, NONE, []), |
|
58 prep_pbt @{theory DiffApp} "pbl_pbla1" [] e_pblID |
|
59 (["pbla1","pbla", "refine", "test"], |
|
60 [("#Given", ["fixedValues a_a","maximum a_1"])], e_rls, NONE, []), |
|
61 prep_pbt @{theory DiffApp} "pbl_pbla2" [] e_pblID |
|
62 (["pbla2","pbla", "refine", "test"], |
|
63 [("#Given", ["fixedValues a_a","valuesFor a_2"])], e_rls, NONE, []), |
|
64 prep_pbt @{theory DiffApp} "pbl_pbla2x" [] e_pblID |
|
65 (["pbla2x","pbla2","pbla", "refine", "test"], |
|
66 [("#Given", ["fixedValues a_a","valuesFor a_2","functionOf a2_x"])], e_rls, NONE, []), |
|
67 prep_pbt @{theory DiffApp} "pbl_pbla2y" [] e_pblID |
|
68 (["pbla2y","pbla2","pbla", "refine", "test"], |
|
69 [("#Given" ,["fixedValues a_a","valuesFor a_2","boundVariable a2_y"])], e_rls, NONE, []), |
|
70 prep_pbt @{theory DiffApp} "pbl_pbla2z" [] e_pblID |
|
71 (["pbla2z","pbla2","pbla", "refine", "test"], |
|
72 [("#Given" ,["fixedValues a_a","valuesFor a_2","interval a2_z"])], e_rls, NONE, []), |
|
73 prep_pbt @{theory DiffApp} "pbl_pbla3" [] e_pblID |
|
74 (["pbla3","pbla", "refine", "test"], |
|
75 [("#Given" ,["fixedValues a_a","relations a_3"])], e_rls, NONE, [])] *} |
48 ML {*"%%%%%%%%%%%%%%%%% start ProgLang.thy %%%%%%%%%%%%%%%%%%%";*} |
76 ML {*"%%%%%%%%%%%%%%%%% start ProgLang.thy %%%%%%%%%%%%%%%%%%%";*} |
49 ML_file "library.sml" |
77 ML_file "library.sml" |
50 ML_file "calcelems.sml" |
78 ML_file "calcelems.sml" |
51 ML_file "kestore.sml" |
79 ML_file "kestore.sml" |
52 ML_file "ProgLang/termC.sml" |
80 ML_file "ProgLang/termC.sml" |
53 |
|
54 setup {* store_pbts |
|
55 [prep_pbt @{theory "Test"} "pbl_ttest" [] e_pblID (["test"], [], e_rls, NONE, []), |
|
56 prep_pbt @{theory "Test"} "pbl_ttest_calc" [] e_pblID |
|
57 (["calculate","test"], |
|
58 [("#Given" ,["realTestGiven t_t"]), |
|
59 ("#Find" ,["realTestFind s_s"])], |
|
60 e_rls, NONE, [["Test","test_calculate"]])] *} |
|
61 |
|
62 ML_file "ProgLang/calculate.sml" |
81 ML_file "ProgLang/calculate.sml" |
63 ML_file "ProgLang/rewrite.sml" |
82 ML_file "ProgLang/rewrite.sml" |
64 ML_file "ProgLang/listC.sml" |
83 ML_file "ProgLang/listC.sml" |
65 ML_file "ProgLang/scrtools.sml" |
84 ML_file "ProgLang/scrtools.sml" |
66 ML_file "ProgLang/tools.sml" |
85 ML_file "ProgLang/tools.sml" |