135 | NONE => ((*writeln"### get_pair: t1 $ t2 -> NONE";*) |
135 | NONE => ((*writeln"### get_pair: t1 $ t2 -> NONE";*) |
136 get_pair thy op_ ef t2) |
136 get_pair thy op_ ef t2) |
137 end; |
137 end; |
138 (* |
138 (* |
139 > val t = (term_of o the o (parse thy)) "#3 + #4"; |
139 > val t = (term_of o the o (parse thy)) "#3 + #4"; |
140 > val eval_fn = the (assoc (!eval_list, "op +")); |
140 > val eval_fn = the (assoc (!eval_list, "Groups.plus_class.plus")); |
141 > val (SOME (id,t')) = get_pair thy "op +" eval_fn t; |
141 > val (SOME (id,t')) = get_pair thy "Groups.plus_class.plus" eval_fn t; |
142 > Syntax.string_of_term (thy2ctxt thy) t'; |
142 > Syntax.string_of_term (thy2ctxt thy) t'; |
143 > atomty t'; |
143 > atomty t'; |
144 > |
144 > |
145 > val t = (term_of o the o (parse thy)) "(a + #3) + #4"; |
145 > val t = (term_of o the o (parse thy)) "(a + #3) + #4"; |
146 > val (SOME (id,t')) = get_pair thy "op +" eval_fn t; |
146 > val (SOME (id,t')) = get_pair thy "Groups.plus_class.plus" eval_fn t; |
147 > Syntax.string_of_term (thy2ctxt thy) t'; |
147 > Syntax.string_of_term (thy2ctxt thy) t'; |
148 > |
148 > |
149 > val t = (term_of o the o (parse thy)) "#3 + (#4 + (a::real))"; |
149 > val t = (term_of o the o (parse thy)) "#3 + (#4 + (a::real))"; |
150 > val (SOME (id,t')) = get_pair thy "op +" eval_fn t; |
150 > val (SOME (id,t')) = get_pair thy "Groups.plus_class.plus" eval_fn t; |
151 > Syntax.string_of_term (thy2ctxt thy) t'; |
151 > Syntax.string_of_term (thy2ctxt thy) t'; |
152 > |
152 > |
153 > val t = (term_of o the o (parse thy)) "x = #5 * (#3 + (#4 + a))"; |
153 > val t = (term_of o the o (parse thy)) "x = #5 * (#3 + (#4 + a))"; |
154 > atomty t; |
154 > atomty t; |
155 > val (SOME (id,t')) = get_pair thy "op +" eval_fn t; |
155 > val (SOME (id,t')) = get_pair thy "Groups.plus_class.plus" eval_fn t; |
156 > Syntax.string_of_term (thy2ctxt thy) t'; |
156 > Syntax.string_of_term (thy2ctxt thy) t'; |
157 > val it = "#3 + (#4 + a) = #7 + a" : string |
157 > val it = "#3 + (#4 + a) = #7 + a" : string |
158 > |
158 > |
159 > |
159 > |
160 > val t = (term_of o the o (parse thy)) "#-4//#-2"; |
160 > val t = (term_of o the o (parse thy)) "#-4//#-2"; |
271 val t = (term_of o the o (parse thy)) "999999999"; |
271 val t = (term_of o the o (parse thy)) "999999999"; |
272 atomty t; |
272 atomty t; |
273 -------------------------------------------------------------------6.8.02: |
273 -------------------------------------------------------------------6.8.02: |
274 |
274 |
275 > val ct = (the o (parse thy)) "a+#3+#4"; |
275 > val ct = (the o (parse thy)) "a+#3+#4"; |
276 > get_calculation_ thy ("op +",the (assoc(!eval_list,"op +"))) ct; |
276 > get_calculation_ thy ("Groups.plus_class.plus",the (assoc(!eval_list,"Groups.plus_class.plus"))) ct; |
277 val it = SOME ("add_3_4","a + 3 + 4 = a + 7 [a + 3 + 4 = a + 7]") |
277 val it = SOME ("add_3_4","a + 3 + 4 = a + 7 [a + 3 + 4 = a + 7]") |
278 |
278 |
279 > val ct = (the o (parse thy)) "#3+(#4+a)"; |
279 > val ct = (the o (parse thy)) "#3+(#4+a)"; |
280 > get_calculation_ thy ("op +",the (assoc(!eval_list,"op +"))) ct; |
280 > get_calculation_ thy ("Groups.plus_class.plus",the (assoc(!eval_list,"Groups.plus_class.plus"))) ct; |
281 val it = SOME ("add_3_4","3 + (4 + a) = 7 + a [3 + (4 + a) = 7 + a]") |
281 val it = SOME ("add_3_4","3 + (4 + a) = 7 + a [3 + (4 + a) = 7 + a]") |
282 |
282 |
283 > val ct = (the o (parse thy)) "a+(#3+#4)+#5"; |
283 > val ct = (the o (parse thy)) "a+(#3+#4)+#5"; |
284 > get_calculation_ thy ("op +",the (assoc(!eval_list,"op +"))) ct; |
284 > get_calculation_ thy ("Groups.plus_class.plus",the (assoc(!eval_list,"Groups.plus_class.plus"))) ct; |
285 val it = SOME ("add_3_4","3 + 4 = 7 [3 + 4 = 7]") : (string * thm) option |
285 val it = SOME ("add_3_4","3 + 4 = 7 [3 + 4 = 7]") : (string * thm) option |
286 |
286 |
287 > val ct = (the o (parse thy)) "#3*(#4*a)"; |
287 > val ct = (the o (parse thy)) "#3*(#4*a)"; |
288 > get_calculation_ thy ("op *",the (assoc(!eval_list,"op *"))) ct; |
288 > get_calculation_ thy ("op *",the (assoc(!eval_list,"op *"))) ct; |
289 val it = SOME ("mult_3_4","3 * (4 * a) = 12 * a [3 * (4 * a) = 12 * a]") |
289 val it = SOME ("mult_3_4","3 * (4 * a) = 12 * a [3 * (4 * a) = 12 * a]") |