90 (Substitute [("a","#2*r*sin alpha"),("b","#2*r*cos alpha")])); |
90 (Substitute [("a","#2*r*sin alpha"),("b","#2*r*cos alpha")])); |
91 "------- same_tacpbl + eval_to -------"; |
91 "------- same_tacpbl + eval_to -------"; |
92 val SOME(l1,t1) = same_tacpbl sc ll (mI1,m1); |
92 val SOME(l1,t1) = same_tacpbl sc ll (mI1,m1); |
93 loc_2str l1; |
93 loc_2str l1; |
94 (*"[R, R, D, R, D, R, D, R, D, R, D, R, D, R, D, L, R]"*) |
94 (*"[R, R, D, R, D, R, D, R, D, R, D, R, D, R, D, L, R]"*) |
95 Sign.string_of_term (sign_of DiffApp.thy) t1; |
95 Syntax.string_of_term (thy2ctxt' "DiffApp") t1; |
96 (*"solve_univar (Reals, [univar, equation], no_met) B.1 B.3 "?6 ?4 *) |
96 (*"solve_univar (Reals, [univar, equation], no_met) B.1 B.3 "?6 ?4 *) |
97 |
97 |
98 val SOME(l2,t2) = same_tacpbl sc l1 (mI2,m2); |
98 val SOME(l2,t2) = same_tacpbl sc l1 (mI2,m2); |
99 loc_2str l2; |
99 loc_2str l2; |
100 (*"[R, R, D, R, D, R, D, R, D, R, D, R, D, R, D, R, D, L, R]"*) |
100 (*"[R, R, D, R, D, R, D, R, D, R, D, R, D, R, D, R, D, L, R]"*) |
101 Sign.string_of_term (sign_of DiffApp.thy) t2; |
101 Syntax.string_of_term (thy2ctxt' "DiffApp") t2; |
102 (*"solve_univar (Reals, [univar, equation], no_met) B.1 B.3 "?7 ?3 *) |
102 (*"solve_univar (Reals, [univar, equation], no_met) B.1 B.3 "?7 ?3 *) |
103 |
103 |
104 val SOME(l3,t3) = same_tacpbl sc l2 (mI3,m3); |
104 val SOME(l3,t3) = same_tacpbl sc l2 (mI3,m3); |
105 loc_2str l3; |
105 loc_2str l3; |
106 (*"[R, R, D, R, D, R, D, R, D, R, D, R, D, R, D, R, D, R, D]"*) |
106 (*"[R, R, D, R, D, R, D, R, D, R, D, R, D, R, D, R, D, R, D]"*) |
107 Sign.string_of_term (sign_of DiffApp.thy) t3; |
107 Syntax.string_of_term (thy2ctxt' "DiffApp") t3; |
108 (*"Substitute [(v_1, (Rhs o hd) B.1), (v_2, (Rhs o hd) B.0)] B.8"*) |
108 (*"Substitute [(v_1, (Rhs o hd) B.1), (v_2, (Rhs o hd) B.0)] B.8"*) |
109 |
109 |
110 |
110 |
111 "------- eq_tacIDs + eq_consts + eval_args -------"; |
111 "------- eq_tacIDs + eq_consts + eval_args -------"; |
112 val eq_ids = eq_tacIDs (*start-loc_*)[] sc (mI,m) []; |
112 val eq_ids = eq_tacIDs (*start-loc_*)[] sc (mI,m) []; |