16 "-calculate.thy: provides 'setup' -----------------------"; |
16 "-calculate.thy: provides 'setup' -----------------------"; |
17 "-calculate.thy: provides 'setup' -----------------------"; |
17 "-calculate.thy: provides 'setup' -----------------------"; |
18 \<close> |
18 \<close> |
19 |
19 |
20 setup \<open>KEStore_Elems.add_pbts |
20 setup \<open>KEStore_Elems.add_pbts |
21 [Specify.prep_pbt @{theory "Test"} "pbl_ttest" [] Celem.e_pblID (["test"], [], Rule_Set.empty, NONE, []), |
21 [Specify.prep_pbt @{theory "Test"} "pbl_ttest" [] Spec.e_pblID (["test"], [], Rule_Set.empty, NONE, []), |
22 Specify.prep_pbt @{theory "Test"} "pbl_ttest_calc" [] Celem.e_pblID |
22 Specify.prep_pbt @{theory "Test"} "pbl_ttest_calc" [] Spec.e_pblID |
23 (["calculate", "test"], |
23 (["calculate", "test"], |
24 [("#Given", ["realTestGiven t_t"]), |
24 [("#Given", ["realTestGiven t_t"]), |
25 ("#Find", ["realTestFind s_s"])], |
25 ("#Find", ["realTestFind s_s"])], |
26 Rule_Set.empty, NONE, [["Test", "test_calculate"]])]\<close> |
26 Rule_Set.empty, NONE, [["Test", "test_calculate"]])]\<close> |
27 |
27 |
32 ((Try (Repeat (Calculate ''PLUS''))) #> |
32 ((Try (Repeat (Calculate ''PLUS''))) #> |
33 (Try (Repeat (Calculate ''TIMES''))) #> |
33 (Try (Repeat (Calculate ''TIMES''))) #> |
34 (Try (Repeat (Calculate ''DIVIDE''))) #> |
34 (Try (Repeat (Calculate ''DIVIDE''))) #> |
35 (Try (Repeat (Calculate ''POWER''))))) t_t" |
35 (Try (Repeat (Calculate ''POWER''))))) t_t" |
36 setup \<open>KEStore_Elems.add_mets |
36 setup \<open>KEStore_Elems.add_mets |
37 [Specify.prep_met (@{theory "Test"}) "met_testcal" [] Celem.e_metID |
37 [Specify.prep_met (@{theory "Test"}) "met_testcal" [] Spec.e_metID |
38 (["Test","test_calculate"], |
38 (["Test","test_calculate"], |
39 [("#Given" , ["realTestGiven t_t"]), ("#Find", ["realTestFind s_s"])], |
39 [("#Given" , ["realTestGiven t_t"]), ("#Find", ["realTestFind s_s"])], |
40 {rew_ord'="sqrt_right",rls'=tval_rls,srls = Rule_Set.empty, prls = Rule_Set.empty, |
40 {rew_ord'="sqrt_right",rls'=tval_rls,srls = Rule_Set.empty, prls = Rule_Set.empty, |
41 calc=[("PLUS", ("op +", eval_binop "#add_")), |
41 calc=[("PLUS", ("op +", eval_binop "#add_")), |
42 ("TIMES", ("Groups.times_class.times", eval_binop "#mult_")), |
42 ("TIMES", ("Groups.times_class.times", eval_binop "#mult_")), |