31 last change by: rlang |
31 last change by: rlang |
32 date: 02.11.29 |
32 date: 02.11.29 |
33 (c) by Richard Lang, 2003\<close> |
33 (c) by Richard Lang, 2003\<close> |
34 |
34 |
35 ML \<open> |
35 ML \<open> |
36 val thy = @{theory}; |
|
37 val ctxt = ThyC.to_ctxt thy; |
|
38 |
|
39 val univariate_equation_prls = |
36 val univariate_equation_prls = |
40 Rule_Set.append_rules "univariate_equation_prls" Rule_Set.empty |
37 Rule_Set.append_rules "univariate_equation_prls" Rule_Set.empty |
41 [Rule.Eval ("Prog_Expr.matches", Prog_Expr.eval_matches "")]; |
38 [Rule.Eval ("Prog_Expr.matches", Prog_Expr.eval_matches "")]; |
42 \<close> |
39 \<close> |
43 rule_set_knowledge univariate_equation_prls = \<open>Auto_Prog.prep_rls @{theory} univariate_equation_prls\<close> |
40 rule_set_knowledge univariate_equation_prls = \<open>Auto_Prog.prep_rls @{theory} univariate_equation_prls\<close> |
63 (* val (h,argl) = strip_comb (str2term "solve (x+1=2, x)"); |
60 (* val (h,argl) = strip_comb (str2term "solve (x+1=2, x)"); |
64 val (h,argl) = strip_comb ((Thm.term_of o the o (parse thy)) |
61 val (h,argl) = strip_comb ((Thm.term_of o the o (parse thy)) |
65 "solveTest (x+1=2, x)"); |
62 "solveTest (x+1=2, x)"); |
66 *) |
63 *) |
67 fun argl2dtss [Const ("Product_Type.Pair", _) $ eq $ bdv] = |
64 fun argl2dtss [Const ("Product_Type.Pair", _) $ eq $ bdv] = |
68 [((the o (TermC.parseNEW ctxt)) "equality", [eq]), |
65 [((the o (TermC.parseNEW \<^context>)) "equality", [eq]), |
69 ((the o (TermC.parseNEW ctxt)) "solveFor", [bdv]), |
66 ((the o (TermC.parseNEW \<^context>)) "solveFor", [bdv]), |
70 ((the o (TermC.parseNEW ctxt)) "solutions", |
67 ((the o (TermC.parseNEW \<^context>)) "solutions", |
71 [(the o (TermC.parseNEW ctxt)) "L"]) |
68 [(the o (TermC.parseNEW \<^context>)) "L"]) |
72 ] |
69 ] |
73 | argl2dtss _ = raise ERROR "Equation.ML: wrong argument for argl2dtss"; |
70 | argl2dtss _ = raise ERROR "Equation.ML: wrong argument for argl2dtss"; |
74 \<close> |
71 \<close> |
75 setup \<open>KEStore_Elems.add_cas |
72 setup \<open>KEStore_Elems.add_cas |
76 [((Thm.term_of o the o (TermC.parse @{theory})) "solveTest", |
73 [((Thm.term_of o the o (TermC.parse @{theory})) "solveTest", |