equal
deleted
inserted
replaced
533 \<close> |
533 \<close> |
534 |
534 |
535 subsection \<open>setup for rule-sets and ML-functions\<close> |
535 subsection \<open>setup for rule-sets and ML-functions\<close> |
536 |
536 |
537 rule_set_knowledge prog_expr = prog_expr |
537 rule_set_knowledge prog_expr = prog_expr |
538 setup \<open>KEStore_Elems.add_calcs |
538 |
539 [("matches", (\<^const_name>\<open>matches\<close>, Prog_Expr.eval_matches "#matches_")), |
539 calculation matches = \<open>Prog_Expr.eval_matches "#matches_"\<close> |
540 ("matchsub", (\<^const_name>\<open>matchsub\<close>, Prog_Expr.eval_matchsub "#matchsub_")), |
540 calculation matchsub = \<open>Prog_Expr.eval_matchsub "#matchsub_"\<close> |
541 ("Vars", (\<^const_name>\<open>Vars\<close>, Prog_Expr.eval_var "#Vars_")), |
541 calculation Vars = \<open>Prog_Expr.eval_var "#Vars_"\<close> |
542 ("lhs", (\<^const_name>\<open>lhs\<close>, Prog_Expr.eval_lhs "")), |
542 calculation lhs = \<open>Prog_Expr.eval_lhs ""\<close> |
543 ("rhs", (\<^const_name>\<open>rhs\<close>, Prog_Expr.eval_rhs ""))]\<close> |
543 calculation rhs = \<open>Prog_Expr.eval_rhs ""\<close> |
544 (*\\------------------------- from Tools .thy-------------------------------------------------//*) |
544 (*\\------------------------- from Tools .thy-------------------------------------------------//*) |
545 ML \<open> |
545 ML \<open> |
546 \<close> ML \<open> |
546 \<close> ML \<open> |
547 \<close> ML \<open> |
547 \<close> ML \<open> |
548 \<close> |
548 \<close> |