equal
deleted
inserted
replaced
493 subsection {* Evaluation *} |
493 subsection {* Evaluation *} |
494 |
494 |
495 ML {* |
495 ML {* |
496 |
496 |
497 local |
497 local |
498 structure Data = Named_Thms(val name = "eval" val description = "evaluation rules"); |
498 structure Data = Named_Thms(val name = @{binding eval} val description = "evaluation rules"); |
499 in |
499 in |
500 |
500 |
501 fun eval_tac ths = |
501 fun eval_tac ths = |
502 Subgoal.FOCUS_PREMS (fn {context, prems, ...} => |
502 Subgoal.FOCUS_PREMS (fn {context, prems, ...} => |
503 DEPTH_SOLVE_1 (resolve_tac (ths @ prems @ Data.get context) 1)); |
503 DEPTH_SOLVE_1 (resolve_tac (ths @ prems @ Data.get context) 1)); |