31 val cal = snd (assoc1 (! calclist', "is_polyexp")); |
31 val cal = snd (assoc1 (! calclist', "is_polyexp")); |
32 val t = @{term "(x / x) is_polyexp"}; |
32 val t = @{term "(x / x) is_polyexp"}; |
33 val SOME (thmID, thm) = get_calculation_ thy cal t; |
33 val SOME (thmID, thm) = get_calculation_ thy cal t; |
34 (HOLogic.dest_Trueprop (prop_of thm); writeln "all thms wrapped by Trueprop") |
34 (HOLogic.dest_Trueprop (prop_of thm); writeln "all thms wrapped by Trueprop") |
35 handle TERM _ => |
35 handle TERM _ => |
36 raise error "calculate.sml: get_calculation_ must return Trueprop"; |
36 error "calculate.sml: get_calculation_ must return Trueprop"; |
37 |
37 |
38 |
38 |
39 |
39 |
40 (*===== inhibit exn ?=========================================================== |
40 (*===== inhibit exn ?=========================================================== |
41 val thy' = "Isac.thy"; |
41 val thy' = "Isac.thy"; |
64 (*it = "#4 ^^^ #2" : string*) |
64 (*it = "#4 ^^^ #2" : string*) |
65 val Some (thmID,thm) = get_calculation_ thy(the(assoc(calclist,"power_")))t; |
65 val Some (thmID,thm) = get_calculation_ thy(the(assoc(calclist,"power_")))t; |
66 val Some (t,_) = rewrite_ thy tless_true tval_rls true thm t; |
66 val Some (t,_) = rewrite_ thy tless_true tval_rls true thm t; |
67 Sign.string_of_term (sign_of thy) t; |
67 Sign.string_of_term (sign_of thy) t; |
68 (*val it = "#16" : string*) |
68 (*val it = "#16" : string*) |
69 if it <> "16" then raise error "calculate.sml: new behaviour in calculate_" |
69 if it <> "16" then error "calculate.sml: new behaviour in calculate_" |
70 else (); |
70 else (); |
71 |
71 |
72 " ================= calculate.sml: aus script ======================== "; |
72 " ================= calculate.sml: aus script ======================== "; |
73 " ================= calculate.sml: aus script ======================== "; |
73 " ================= calculate.sml: aus script ======================== "; |
74 " ================= calculate.sml: aus script ======================== "; |
74 " ================= calculate.sml: aus script ======================== "; |
138 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
138 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
139 (*nxt = ("Check_Postcond",Check_Postcond ["calculate","test"])*) |
139 (*nxt = ("Check_Postcond",Check_Postcond ["calculate","test"])*) |
140 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
140 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
141 (*nxt = ("End_Proof'",End_Proof')*) |
141 (*nxt = ("End_Proof'",End_Proof')*) |
142 if f = Form' (FormKF (~1,EdUndef,0,Nundef,"16")) then () |
142 if f = Form' (FormKF (~1,EdUndef,0,Nundef,"16")) then () |
143 else raise error "calculate.sml: script test_calculate changed behaviour"; |
143 else error "calculate.sml: script test_calculate changed behaviour"; |
144 |
144 |
145 |
145 |
146 |
146 |
147 |
147 |
148 " ================= calculate.sml: 2.8.02 check test-root-equ ======== "; |
148 " ================= calculate.sml: 2.8.02 check test-root-equ ======== "; |
419 val Some (thmID,thm) = get_calculation_ thy(the(assoc(calclist,"power_")))t; |
419 val Some (thmID,thm) = get_calculation_ thy(the(assoc(calclist,"power_")))t; |
420 "4 ^^^ 2 = 16"; |
420 "4 ^^^ 2 = 16"; |
421 val Some (t,_) = rewrite_ thy tless_true tval_rls true thm t; |
421 val Some (t,_) = rewrite_ thy tless_true tval_rls true thm t; |
422 Sign.string_of_term (sign_of thy) t; |
422 Sign.string_of_term (sign_of thy) t; |
423 "16"; |
423 "16"; |
424 if it <> "16" then raise error "calculate.sml: new behaviour in calculate_" |
424 if it <> "16" then error "calculate.sml: new behaviour in calculate_" |
425 else (); |
425 else (); |
426 |
426 |
427 (*13.9.02 *** calc: operator = pow not defined*) |
427 (*13.9.02 *** calc: operator = pow not defined*) |
428 val t = (term_of o the o (parse thy)) "3^^^2"; |
428 val t = (term_of o the o (parse thy)) "3^^^2"; |
429 val Some (thmID,thm) = |
429 val Some (thmID,thm) = |
456 "[] from_ [c, c_2, c_3, c_4] occur_exactly_in -1 * (q_0 * L ^^^ 2) / 2" |
456 "[] from_ [c, c_2, c_3, c_4] occur_exactly_in -1 * (q_0 * L ^^^ 2) / 2" |
457 ); |
457 ); |
458 val Some (str, simpl) = get_pair thy op_ ef arg; |
458 val Some (str, simpl) = get_pair thy op_ ef arg; |
459 if str = |
459 if str = |
460 "[] from_ [c, c_2, c_3, c_4] occur_exactly_in -1 * (q_0 * L ^^^ 2) / 2 = True" |
460 "[] from_ [c, c_2, c_3, c_4] occur_exactly_in -1 * (q_0 * L ^^^ 2) / 2 = True" |
461 then () else raise error "calculate.sml get_pair with 3 args:occur_exactly_in"; |
461 then () else error "calculate.sml get_pair with 3 args:occur_exactly_in"; |
462 |
462 |
463 |
463 |
464 |
464 |
465 " ================= eval_binop Float =================== "; |
465 " ================= eval_binop Float =================== "; |
466 val t = str2term "Float ((1,2),(0,0))"; |
466 val t = str2term "Float ((1,2),(0,0))"; |