equal
deleted
inserted
replaced
568 val ttt = (term_of o the o (parse (Thy_Info.get_theory "Isac"))) "(matches ( v_v = 0) e_e)"; |
568 val ttt = (term_of o the o (parse (Thy_Info.get_theory "Isac"))) "(matches ( v_v = 0) e_e)"; |
569 |
569 |
570 ------ 25.8.01*) |
570 ------ 25.8.01*) |
571 |
571 |
572 *} |
572 *} |
573 setup {* KEStore_Elems.store_pbts |
573 setup {* KEStore_Elems.add_pbts |
574 [(prep_pbt thy "pbl_test" [] e_pblID (["test"], [], e_rls, NONE, [])), |
574 [(prep_pbt thy "pbl_test" [] e_pblID (["test"], [], e_rls, NONE, [])), |
575 (prep_pbt thy "pbl_test_equ" [] e_pblID |
575 (prep_pbt thy "pbl_test_equ" [] e_pblID |
576 (["equation","test"], |
576 (["equation","test"], |
577 [("#Given" ,["equality e_e","solveFor v_v"]), |
577 [("#Given" ,["equality e_e","solveFor v_v"]), |
578 ("#Where" ,["matches (?a = ?b) e_e"]), |
578 ("#Where" ,["matches (?a = ?b) e_e"]), |
829 val ct = "HOL.True" : cterm |
829 val ct = "HOL.True" : cterm |
830 |
830 |
831 *) |
831 *) |
832 |
832 |
833 *} |
833 *} |
834 setup {* KEStore_Elems.store_pbts |
834 setup {* KEStore_Elems.add_pbts |
835 [(prep_pbt thy "pbl_test_uni_plain2" [] e_pblID |
835 [(prep_pbt thy "pbl_test_uni_plain2" [] e_pblID |
836 (["plain_square","univariate","equation","test"], |
836 (["plain_square","univariate","equation","test"], |
837 [("#Given" ,["equality e_e","solveFor v_v"]), |
837 [("#Given" ,["equality e_e","solveFor v_v"]), |
838 ("#Where" ,["(matches (?a + ?b*v_v ^^^2 = 0) e_e) |" ^ |
838 ("#Where" ,["(matches (?a + ?b*v_v ^^^2 = 0) e_e) |" ^ |
839 "(matches ( ?b*v_v ^^^2 = 0) e_e) |" ^ |
839 "(matches ( ?b*v_v ^^^2 = 0) e_e) |" ^ |
919 show_ptyps(); |
919 show_ptyps(); |
920 get_pbt ["inttype","test"]; |
920 get_pbt ["inttype","test"]; |
921 *) |
921 *) |
922 |
922 |
923 *} |
923 *} |
924 setup {* KEStore_Elems.store_pbts |
924 setup {* KEStore_Elems.add_pbts |
925 [(prep_pbt thy "pbl_test_uni_poly" [] e_pblID |
925 [(prep_pbt thy "pbl_test_uni_poly" [] e_pblID |
926 (["polynomial","univariate","equation","test"], |
926 (["polynomial","univariate","equation","test"], |
927 [("#Given" ,["equality (v_v ^^^2 + p_p * v_v + q__q = 0)","solveFor v_v"]), |
927 [("#Given" ,["equality (v_v ^^^2 + p_p * v_v + q__q = 0)","solveFor v_v"]), |
928 ("#Where" ,["HOL.False"]), |
928 ("#Where" ,["HOL.False"]), |
929 ("#Find" ,["solutions v_v'i'"])], |
929 ("#Find" ,["solutions v_v'i'"])], |