equal
deleted
inserted
replaced
216 *) |
216 *) |
217 fun eval_get_denominator (thmid:string) _ |
217 fun eval_get_denominator (thmid:string) _ |
218 (t as Const ("Rational.get_denominator", _) $ |
218 (t as Const ("Rational.get_denominator", _) $ |
219 (Const ("Fields.inverse_class.divide", _) $num |
219 (Const ("Fields.inverse_class.divide", _) $num |
220 $denom)) thy = |
220 $denom)) thy = |
221 SOME (mk_thmid thmid "" |
221 SOME (mk_thmid thmid "" (term_to_string''' thy denom) "", |
222 (Print_Mode.setmp [] |
222 Trueprop $ (mk_equality (t, denom))) |
223 (Syntax.string_of_term (thy2ctxt thy)) denom) "", |
|
224 Trueprop $ (mk_equality (t, denom))) |
|
225 | eval_get_denominator _ _ _ _ = NONE; |
223 | eval_get_denominator _ _ _ _ = NONE; |
226 *} |
224 *} |
227 text {*\noindent For the tests of \ttfamily eval\_get\_denominator \normalfont |
225 text {*\noindent For the tests of \ttfamily eval\_get\_denominator \normalfont |
228 see \ttfamily test/Knowledge/rational.sml\normalfont*} |
226 see \ttfamily test/Knowledge/rational.sml\normalfont*} |
229 |
227 |
238 *) |
236 *) |
239 fun eval_get_numerator (thmid:string) _ |
237 fun eval_get_numerator (thmid:string) _ |
240 (t as Const ("Rational.get_numerator", _) $ |
238 (t as Const ("Rational.get_numerator", _) $ |
241 (Const ("Fields.inverse_class.divide", _) $num |
239 (Const ("Fields.inverse_class.divide", _) $num |
242 $denom )) thy = |
240 $denom )) thy = |
243 SOME (mk_thmid thmid "" |
241 SOME (mk_thmid thmid "" (term_to_string''' thy num) "", |
244 (Print_Mode.setmp [] |
242 Trueprop $ (mk_equality (t, num))) |
245 (Syntax.string_of_term (thy2ctxt thy)) num) "", |
|
246 Trueprop $ (mk_equality (t, num))) |
|
247 | eval_get_numerator _ _ _ _ = NONE; |
243 | eval_get_numerator _ _ _ _ = NONE; |
248 *} |
244 *} |
249 |
245 |
250 text {*\noindent We discovered several problems by implementing the |
246 text {*\noindent We discovered several problems by implementing the |
251 \ttfamily get\_numerator \normalfont function. Remember when |
247 \ttfamily get\_numerator \normalfont function. Remember when |
444 eval_factors_from_solution ""))*) |
440 eval_factors_from_solution ""))*) |
445 |
441 |
446 fun eval_factors_from_solution (thmid:string) _ |
442 fun eval_factors_from_solution (thmid:string) _ |
447 (t as Const ("Partial_Fractions.factors_from_solution", _) $ sol) |
443 (t as Const ("Partial_Fractions.factors_from_solution", _) $ sol) |
448 thy = ((let val prod = factors_from_solution sol |
444 thy = ((let val prod = factors_from_solution sol |
449 in SOME (mk_thmid thmid "" |
445 in SOME (mk_thmid thmid "" (term_to_string''' thy prod) "", |
450 (Print_Mode.setmp [] |
|
451 (Syntax.string_of_term (thy2ctxt thy)) prod) "", |
|
452 Trueprop $ (mk_equality (t, prod))) |
446 Trueprop $ (mk_equality (t, prod))) |
453 end) |
447 end) |
454 handle _ => NONE) |
448 handle _ => NONE) |
455 | eval_factors_from_solution _ _ _ _ = NONE; |
449 | eval_factors_from_solution _ _ _ _ = NONE; |
456 *} |
450 *} |