equal
deleted
inserted
replaced
430 |
430 |
431 fun refine_insert ths = |
431 fun refine_insert ths = |
432 refine_singleton (Method.Basic (K (Method.insert ths))); |
432 refine_singleton (Method.Basic (K (Method.insert ths))); |
433 |
433 |
434 fun refine_primitive r = |
434 fun refine_primitive r = |
435 refine_singleton (Method.Basic (fn ctxt => fn _ => Method.CONTEXT_TACTIC (PRIMITIVE (r ctxt)))); |
435 refine_singleton (Method.Basic (fn ctxt => fn _ => CONTEXT_TACTIC (PRIMITIVE (r ctxt)))); |
436 |
436 |
437 end; |
437 end; |
438 |
438 |
439 |
439 |
440 (* refine via sub-proof *) |
440 (* refine via sub-proof *) |
971 val explicit_vars = fold Term.add_vars var_props []; |
971 val explicit_vars = fold Term.add_vars var_props []; |
972 val vars = filter_out (member (op =) explicit_vars) (fold Term.add_vars props []); |
972 val vars = filter_out (member (op =) explicit_vars) (fold Term.add_vars props []); |
973 in map (Logic.mk_term o Var) vars end; |
973 in map (Logic.mk_term o Var) vars end; |
974 |
974 |
975 fun refine_terms n = |
975 fun refine_terms n = |
976 refine_singleton (Method.Basic (fn ctxt => Method.CONTEXT_TACTIC o |
976 refine_singleton (Method.Basic (fn ctxt => CONTEXT_TACTIC o |
977 K (HEADGOAL (PRECISE_CONJUNCTS n |
977 K (HEADGOAL (PRECISE_CONJUNCTS n |
978 (HEADGOAL (CONJUNCTS (ALLGOALS (resolve_tac ctxt [Drule.termI])))))))); |
978 (HEADGOAL (CONJUNCTS (ALLGOALS (resolve_tac ctxt [Drule.termI])))))))); |
979 |
979 |
980 in |
980 in |
981 |
981 |