678 ("succeed", no_args succeed, "succeed"), |
678 ("succeed", no_args succeed, "succeed"), |
679 ("-", no_args insert_facts, "do nothing (insert current facts only)"), |
679 ("-", no_args insert_facts, "do nothing (insert current facts only)"), |
680 ("insert", thms_args insert, "insert theorems, ignoring facts (improper)"), |
680 ("insert", thms_args insert, "insert theorems, ignoring facts (improper)"), |
681 ("unfold", thms_args unfold, "unfold definitions"), |
681 ("unfold", thms_args unfold, "unfold definitions"), |
682 ("fold", thms_args fold, "fold definitions"), |
682 ("fold", thms_args fold, "fold definitions"), |
683 ("atomize", no_args (SIMPLE_METHOD' HEADGOAL ObjectLogic.atomize_tac), |
683 ("atomize", no_args (SIMPLE_METHOD' HEADGOAL (CHANGED_PROP o ObjectLogic.atomize_tac)), |
684 "present local premises as object-level statements"), |
684 "present local premises as object-level statements"), |
685 ("rule", thms_ctxt_args some_rule, "apply some rule"), |
685 ("rule", thms_ctxt_args some_rule, "apply some rule"), |
686 ("erule", nat_thms_args erule, "apply rule in elimination manner (improper)"), |
686 ("erule", nat_thms_args erule, "apply rule in elimination manner (improper)"), |
687 ("drule", nat_thms_args drule, "apply rule in destruct manner (improper)"), |
687 ("drule", nat_thms_args drule, "apply rule in destruct manner (improper)"), |
688 ("frule", nat_thms_args frule, "apply rule in forward manner (improper)"), |
688 ("frule", nat_thms_args frule, "apply rule in forward manner (improper)"), |