34 val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"plus"))) t; |
34 val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"plus"))) t; |
35 |
35 |
36 val t = (term_of o the o (parse thy)) "((1+2)*4/3)^^^2"; |
36 val t = (term_of o the o (parse thy)) "((1+2)*4/3)^^^2"; |
37 val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"plus"))) t; |
37 val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"plus"))) t; |
38 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; |
38 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; |
39 Sign.string_of_term (sign_of thy) t; |
39 Syntax.string_of_term (thy2ctxt thy) t; |
40 (*val it = "(#3 * #4 // #3) ^^^ #2" : string*) |
40 (*val it = "(#3 * #4 // #3) ^^^ #2" : string*) |
41 val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"times"))) t; |
41 val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"times"))) t; |
42 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; |
42 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; |
43 Sign.string_of_term (sign_of thy) t; |
43 Syntax.string_of_term (thy2ctxt thy) t; |
44 (*val it = "(#12 // #3) ^^^ #2" : string*) |
44 (*val it = "(#12 // #3) ^^^ #2" : string*) |
45 val SOME (thmID,thm) = get_calculation_ thy(the(assoc(calclist,"divide_")))t; |
45 val SOME (thmID,thm) = get_calculation_ thy(the(assoc(calclist,"divide_")))t; |
46 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; |
46 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; |
47 Sign.string_of_term (sign_of thy) t; |
47 Syntax.string_of_term (thy2ctxt thy) t; |
48 (*it = "#4 ^^^ #2" : string*) |
48 (*it = "#4 ^^^ #2" : string*) |
49 val SOME (thmID,thm) = get_calculation_ thy(the(assoc(calclist,"power_")))t; |
49 val SOME (thmID,thm) = get_calculation_ thy(the(assoc(calclist,"power_")))t; |
50 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; |
50 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; |
51 Sign.string_of_term (sign_of thy) t; |
51 Syntax.string_of_term (thy2ctxt thy) t; |
52 (*val it = "#16" : string*) |
52 (*val it = "#16" : string*) |
53 if it <> "16" then raise error "calculate.sml: new behaviour in calculate_" |
53 if it <> "16" then raise error "calculate.sml: new behaviour in calculate_" |
54 else (); |
54 else (); |
55 |
55 |
56 " ================= calculate.sml: aus script ======================== "; |
56 " ================= calculate.sml: aus script ======================== "; |
386 |
386 |
387 val t = (term_of o the o (parse thy)) "((1 + 2) * 4 / 3) ^^^ 2"; |
387 val t = (term_of o the o (parse thy)) "((1 + 2) * 4 / 3) ^^^ 2"; |
388 val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"plus"))) t; |
388 val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"plus"))) t; |
389 "1 + 2 = 3"; |
389 "1 + 2 = 3"; |
390 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; |
390 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; |
391 Sign.string_of_term (sign_of thy) t; |
391 Syntax.string_of_term (thy2ctxt thy) t; |
392 "(3 * 4 / 3) ^^^ 2"; |
392 "(3 * 4 / 3) ^^^ 2"; |
393 val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"times")))t; |
393 val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"times")))t; |
394 "3 * 4 = 12"; |
394 "3 * 4 = 12"; |
395 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; |
395 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; |
396 Sign.string_of_term (sign_of thy) t; |
396 Syntax.string_of_term (thy2ctxt thy) t; |
397 "(12 / 3) ^^^ 2"; |
397 "(12 / 3) ^^^ 2"; |
398 val SOME (thmID,thm) =get_calculation_ thy(the(assoc(calclist,"divide_")))t; |
398 val SOME (thmID,thm) =get_calculation_ thy(the(assoc(calclist,"divide_")))t; |
399 "12 / 3 = 4"; |
399 "12 / 3 = 4"; |
400 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; |
400 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; |
401 Sign.string_of_term (sign_of thy) t; |
401 Syntax.string_of_term (thy2ctxt thy) t; |
402 "4 ^^^ 2"; |
402 "4 ^^^ 2"; |
403 val SOME (thmID,thm) = get_calculation_ thy(the(assoc(calclist,"power_")))t; |
403 val SOME (thmID,thm) = get_calculation_ thy(the(assoc(calclist,"power_")))t; |
404 "4 ^^^ 2 = 16"; |
404 "4 ^^^ 2 = 16"; |
405 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; |
405 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; |
406 Sign.string_of_term (sign_of thy) t; |
406 Syntax.string_of_term (thy2ctxt thy) t; |
407 "16"; |
407 "16"; |
408 if it <> "16" then raise error "calculate.sml: new behaviour in calculate_" |
408 if it <> "16" then raise error "calculate.sml: new behaviour in calculate_" |
409 else (); |
409 else (); |
410 |
410 |
411 (*13.9.02 *** calc: operator = pow not defined*) |
411 (*13.9.02 *** calc: operator = pow not defined*) |