equal
deleted
inserted
replaced
57 |
57 |
58 (*("factors_from_solution", ("Partial_Fractions.factors_from_solution", |
58 (*("factors_from_solution", ("Partial_Fractions.factors_from_solution", |
59 eval_factors_from_solution "")) |
59 eval_factors_from_solution "")) |
60 this code is limited (max 3 solutions) AND has too little checks *) |
60 this code is limited (max 3 solutions) AND has too little checks *) |
61 fun eval_factors_from_solution (thmid:string) _ |
61 fun eval_factors_from_solution (thmid:string) _ |
62 (t as Const (\<^const_name>\<open>Partial_Fractions.factors_from_solution\<close>, _) $ sol) thy = |
62 (t as Const (\<^const_name>\<open>Partial_Fractions.factors_from_solution\<close>, _) $ sol) ctxt = |
63 let val prod = factors_from_solution sol |
63 let val prod = factors_from_solution sol |
64 in SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy prod) "", |
64 in SOME (TermC.mk_thmid thmid (UnparseC.term_in_ctxt ctxt prod) "", |
65 HOLogic.Trueprop $ (TermC.mk_equality (t, prod))) |
65 HOLogic.Trueprop $ (TermC.mk_equality (t, prod))) |
66 end |
66 end |
67 | eval_factors_from_solution _ _ _ _ = NONE; |
67 | eval_factors_from_solution _ _ _ _ = NONE; |
68 \<close> |
68 \<close> |
69 |
69 |