equal
deleted
inserted
replaced
57 Rule.Eval ("Prog_Expr.occurs_in", Prog_Expr.eval_occurs_in ""), |
57 Rule.Eval ("Prog_Expr.occurs_in", Prog_Expr.eval_occurs_in ""), |
58 Rule.Eval ("Prog_Expr.matches", Prog_Expr.eval_matches "")], |
58 Rule.Eval ("Prog_Expr.matches", Prog_Expr.eval_matches "")], |
59 scr = Rule.Empty_Prog |
59 scr = Rule.Empty_Prog |
60 }); |
60 }); |
61 \<close> |
61 \<close> |
62 setup_rule eval_rls = \<open>eval_rls\<close> |
62 rule_set_knowledge eval_rls = \<open>eval_rls\<close> |
63 |
63 |
64 (** problem types **) |
64 (** problem types **) |
65 setup \<open>KEStore_Elems.add_pbts |
65 setup \<open>KEStore_Elems.add_pbts |
66 [(Problem.prep_input thy "pbl_fun_max" [] Problem.id_empty |
66 [(Problem.prep_input thy "pbl_fun_max" [] Problem.id_empty |
67 (["maximum_of", "function"], |
67 (["maximum_of", "function"], |
197 ML \<open> |
197 ML \<open> |
198 val prog_expr = Rule_Set.append_rules "prog_expr" prog_expr |
198 val prog_expr = Rule_Set.append_rules "prog_expr" prog_expr |
199 [Rule.Thm ("filterVar_Const", ThmC.numerals_to_Free @{thm filterVar_Const}), |
199 [Rule.Thm ("filterVar_Const", ThmC.numerals_to_Free @{thm filterVar_Const}), |
200 Rule.Thm ("filterVar_Nil", ThmC.numerals_to_Free @{thm filterVar_Nil})]; |
200 Rule.Thm ("filterVar_Nil", ThmC.numerals_to_Free @{thm filterVar_Nil})]; |
201 \<close> |
201 \<close> |
202 setup_rule prog_expr = \<open>prog_expr\<close> |
202 rule_set_knowledge prog_expr = \<open>prog_expr\<close> |
203 ML \<open> |
203 ML \<open> |
204 \<close> ML \<open> |
204 \<close> ML \<open> |
205 \<close> ML \<open> |
205 \<close> ML \<open> |
206 \<close> |
206 \<close> |
207 end |
207 end |