equal
deleted
inserted
replaced
1055 |
1055 |
1056 |
1056 |
1057 (* METHOD_CLASET' *) |
1057 (* METHOD_CLASET' *) |
1058 |
1058 |
1059 fun METHOD_CLASET' tac ctxt = |
1059 fun METHOD_CLASET' tac ctxt = |
1060 Method.METHOD (FIRSTGOAL o tac (get_local_claset ctxt)); |
1060 Method.METHOD (FINDGOAL o tac (get_local_claset ctxt)); |
1061 |
1061 |
1062 |
1062 |
1063 val trace_rules = ref false; |
1063 val trace_rules = ref false; |
1064 |
1064 |
1065 local |
1065 local |
1147 |
1147 |
1148 fun cla_meth tac prems ctxt = Method.METHOD (fn facts => |
1148 fun cla_meth tac prems ctxt = Method.METHOD (fn facts => |
1149 ALLGOALS (Method.insert_tac (prems @ facts)) THEN tac (get_local_claset ctxt)); |
1149 ALLGOALS (Method.insert_tac (prems @ facts)) THEN tac (get_local_claset ctxt)); |
1150 |
1150 |
1151 fun cla_meth' tac prems ctxt = Method.METHOD (fn facts => |
1151 fun cla_meth' tac prems ctxt = Method.METHOD (fn facts => |
1152 FIRSTGOAL (Method.insert_tac (prems @ facts) THEN' tac (get_local_claset ctxt))); |
1152 FINDGOAL (Method.insert_tac (prems @ facts) THEN' tac (get_local_claset ctxt))); |
1153 |
1153 |
1154 val cla_method = Method.bang_sectioned_args cla_modifiers o cla_meth; |
1154 val cla_method = Method.bang_sectioned_args cla_modifiers o cla_meth; |
1155 val cla_method' = Method.bang_sectioned_args cla_modifiers o cla_meth'; |
1155 val cla_method' = Method.bang_sectioned_args cla_modifiers o cla_meth'; |
1156 |
1156 |
1157 |
1157 |