34 | NONE => error "diophanteq.sml: syntax error in rewriting for usecase1"; |
34 | NONE => error "diophanteq.sml: syntax error in rewriting for usecase1"; |
35 |
35 |
36 val SOME (t,_) = rewrite_inst_ thy e_rew_ord e_rls true subst |
36 val SOME (t,_) = rewrite_inst_ thy e_rew_ord e_rls true subst |
37 (num_str @{thm "int_isolate_add"}) t; term2str t; |
37 (num_str @{thm "int_isolate_add"}) t; term2str t; |
38 |
38 |
39 val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"TIMES"))) t; |
39 val SOME (thmID,thm) = adhoc_thm thy (the(assoc(calclist,"TIMES"))) t; |
40 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; term2str t; |
40 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; term2str t; |
41 |
41 |
42 val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"PLUS"))) t; |
42 val SOME (thmID,thm) = adhoc_thm thy (the(assoc(calclist,"PLUS"))) t; |
43 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; term2str t; |
43 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; term2str t; |
44 |
44 |
45 "----------- mathengine with usecase1 -------------------"; |
45 "----------- mathengine with usecase1 -------------------"; |
46 "----------- mathengine with usecase1 -------------------"; |
46 "----------- mathengine with usecase1 -------------------"; |
47 "----------- mathengine with usecase1 -------------------"; |
47 "----------- mathengine with usecase1 -------------------"; |
69 |
69 |
70 val t = case parseNEW ctxt "xxx + abc + -1 * 111 + (123::int)" of |
70 val t = case parseNEW ctxt "xxx + abc + -1 * 111 + (123::int)" of |
71 SOME t' => t' |
71 SOME t' => t' |
72 | NONE => error "diophanteq.sml: syntax error in rewriting for usecase2"; |
72 | NONE => error "diophanteq.sml: syntax error in rewriting for usecase2"; |
73 |
73 |
74 val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"TIMES"))) t; |
74 val SOME (thmID,thm) = adhoc_thm thy (the(assoc(calclist,"TIMES"))) t; |
75 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; term2str t; |
75 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; term2str t; |
76 |
76 |
77 val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"PLUS"))) t; |
77 val SOME (thmID,thm) = adhoc_thm thy (the(assoc(calclist,"PLUS"))) t; |
78 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; term2str t; |
78 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; term2str t; |
79 |
79 |
80 |
80 |
81 "----------- mathengine with usecase2 -------------------"; |
81 "----------- mathengine with usecase2 -------------------"; |
82 "----------- mathengine with usecase2 -------------------"; |
82 "----------- mathengine with usecase2 -------------------"; |