552 fun goal_args_ctxt args tac = goal_args_ctxt' (Scan.lift args) tac; |
552 fun goal_args_ctxt args tac = goal_args_ctxt' (Scan.lift args) tac; |
553 |
553 |
554 |
554 |
555 (* theory setup *) |
555 (* theory setup *) |
556 |
556 |
557 val _ = Context.>> (add_methods |
557 val _ = Context.>> (Context.map_theory |
558 [("fail", no_args fail, "force failure"), |
558 (add_methods |
559 ("succeed", no_args succeed, "succeed"), |
559 [("fail", no_args fail, "force failure"), |
560 ("-", no_args insert_facts, "do nothing (insert current facts only)"), |
560 ("succeed", no_args succeed, "succeed"), |
561 ("insert", thms_args insert, "insert theorems, ignoring facts (improper)"), |
561 ("-", no_args insert_facts, "do nothing (insert current facts only)"), |
562 ("intro", thms_args intro, "repeatedly apply introduction rules"), |
562 ("insert", thms_args insert, "insert theorems, ignoring facts (improper)"), |
563 ("elim", thms_args elim, "repeatedly apply elimination rules"), |
563 ("intro", thms_args intro, "repeatedly apply introduction rules"), |
564 ("unfold", thms_ctxt_args unfold_meth, "unfold definitions"), |
564 ("elim", thms_args elim, "repeatedly apply elimination rules"), |
565 ("fold", thms_ctxt_args fold_meth, "fold definitions"), |
565 ("unfold", thms_ctxt_args unfold_meth, "unfold definitions"), |
566 ("atomize", (atomize o fst) oo syntax (Args.mode "full"), |
566 ("fold", thms_ctxt_args fold_meth, "fold definitions"), |
567 "present local premises as object-level statements"), |
567 ("atomize", (atomize o fst) oo syntax (Args.mode "full"), |
568 ("iprover", iprover_meth, "intuitionistic proof search"), |
568 "present local premises as object-level statements"), |
569 ("rule", thms_ctxt_args some_rule, "apply some intro/elim rule"), |
569 ("iprover", iprover_meth, "intuitionistic proof search"), |
570 ("erule", nat_thms_args erule, "apply rule in elimination manner (improper)"), |
570 ("rule", thms_ctxt_args some_rule, "apply some intro/elim rule"), |
571 ("drule", nat_thms_args drule, "apply rule in destruct manner (improper)"), |
571 ("erule", nat_thms_args erule, "apply rule in elimination manner (improper)"), |
572 ("frule", nat_thms_args frule, "apply rule in forward manner (improper)"), |
572 ("drule", nat_thms_args drule, "apply rule in destruct manner (improper)"), |
573 ("this", no_args this, "apply current facts as rules"), |
573 ("frule", nat_thms_args frule, "apply rule in forward manner (improper)"), |
574 ("fact", thms_ctxt_args fact, "composition by facts from context"), |
574 ("this", no_args this, "apply current facts as rules"), |
575 ("assumption", ctxt_args assumption, "proof by assumption, preferring facts"), |
575 ("fact", thms_ctxt_args fact, "composition by facts from context"), |
576 ("rename_tac", goal_args (Scan.repeat1 Args.name) Tactic.rename_params_tac, |
576 ("assumption", ctxt_args assumption, "proof by assumption, preferring facts"), |
577 "rename parameters of goal"), |
577 ("rename_tac", goal_args (Scan.repeat1 Args.name) Tactic.rename_params_tac, |
578 ("rotate_tac", goal_args (Scan.optional Args.int 1) Tactic.rotate_tac, |
578 "rename parameters of goal"), |
579 "rotate assumptions of goal"), |
579 ("rotate_tac", goal_args (Scan.optional Args.int 1) Tactic.rotate_tac, |
580 ("tactic", simple_args (Args.position Args.name) tactic, "ML tactic as proof method"), |
580 "rotate assumptions of goal"), |
581 ("raw_tactic", simple_args (Args.position Args.name) raw_tactic, "ML tactic as raw proof method")]); |
581 ("tactic", simple_args (Args.position Args.name) tactic, "ML tactic as proof method"), |
|
582 ("raw_tactic", simple_args (Args.position Args.name) raw_tactic, |
|
583 "ML tactic as raw proof method")])); |
582 |
584 |
583 |
585 |
584 (* outer parser *) |
586 (* outer parser *) |
585 |
587 |
586 local |
588 local |