equal
deleted
inserted
replaced
41 |
41 |
42 (** CAS-command **) |
42 (** CAS-command **) |
43 |
43 |
44 (*.function for handling the cas-input "Simplify (2*a + 3*a)": |
44 (*.function for handling the cas-input "Simplify (2*a + 3*a)": |
45 make a model which is already in ctree-internal format.*) |
45 make a model which is already in ctree-internal format.*) |
46 (* val (h,argl) = strip_comb (str2term "Simplify (2*a + 3*a)"); |
46 (* val (h,argl) = strip_comb (TermC.parse_test @{context} "Simplify (2*a + 3*a)"); |
47 val (h,argl) = strip_comb ((Thm.term_of o the o (parse (Thy_Info_get_theory "Simplify"))) |
47 val (h,argl) = strip_comb ((Thm.term_of o the o (parse (Thy_Info_get_theory "Simplify"))) |
48 "Simplify (2*a + 3*a)"); |
48 "Simplify (2*a + 3*a)"); |
49 *) |
49 *) |
50 fun argl2dtss t = |
50 fun argl2dtss t = |
51 [((TermC.parseNEW''\<^theory>) "Term", t), |
51 [((TermC.parseNEW''\<^theory>) "Term", t), |