equal
deleted
inserted
replaced
242 |
242 |
243 ML \<open> |
243 ML \<open> |
244 (** CAS-commands **) |
244 (** CAS-commands **) |
245 |
245 |
246 (*.handle cas-input like "Diff (a * x^3 + b, x)".*) |
246 (*.handle cas-input like "Diff (a * x^3 + b, x)".*) |
247 (* val (t, pairl) = strip_comb (str2term "Diff (a * x^3 + b, x)"); |
247 (* val (t, pairl) = strip_comb (TermC.parse_test @{context} "Diff (a * x^3 + b, x)"); |
248 val [Const (\<^const_name>\<open>Pair\<close>, _) $ t $ bdv] = pairl; |
248 val [Const (\<^const_name>\<open>Pair\<close>, _) $ t $ bdv] = pairl; |
249 *) |
249 *) |
250 fun argl2dtss [Const (\<^const_name>\<open>Pair\<close>, _) $ t $ bdv] = |
250 fun argl2dtss [Const (\<^const_name>\<open>Pair\<close>, _) $ t $ bdv] = |
251 [((TermC.parseNEW''\<^theory>) "functionTerm", [t]), |
251 [((TermC.parseNEW''\<^theory>) "functionTerm", [t]), |
252 ((TermC.parseNEW''\<^theory>) "differentiateFor", [bdv]), |
252 ((TermC.parseNEW''\<^theory>) "differentiateFor", [bdv]), |
388 Problem_Ref: "derivative_of/function" |
388 Problem_Ref: "derivative_of/function" |
389 |
389 |
390 ML \<open> |
390 ML \<open> |
391 |
391 |
392 (*.handle cas-input like "Differentiate (A = s * (a - s), s)".*) |
392 (*.handle cas-input like "Differentiate (A = s * (a - s), s)".*) |
393 (* val (t, pairl) = strip_comb (str2term "Differentiate (A = s * (a - s), s)"); |
393 (* val (t, pairl) = strip_comb (TermC.parse_test @{context} "Differentiate (A = s * (a - s), s)"); |
394 val [Const (\<^const_name>\<open>Pair\<close>, _) $ t $ bdv] = pairl; |
394 val [Const (\<^const_name>\<open>Pair\<close>, _) $ t $ bdv] = pairl; |
395 *) |
395 *) |
396 fun argl2dtss [Const (\<^const_name>\<open>Pair\<close>, _) $ t $ bdv] = |
396 fun argl2dtss [Const (\<^const_name>\<open>Pair\<close>, _) $ t $ bdv] = |
397 [((TermC.parseNEW''\<^theory>) "functionEq", [t]), |
397 [((TermC.parseNEW''\<^theory>) "functionEq", [t]), |
398 ((TermC.parseNEW''\<^theory>) "differentiateFor", [bdv]), |
398 ((TermC.parseNEW''\<^theory>) "differentiateFor", [bdv]), |