equal
deleted
inserted
replaced
85 |
85 |
86 in |
86 in |
87 |
87 |
88 fun method_setup name = |
88 fun method_setup name = |
89 Method.setup name |
89 Method.setup name |
90 (Args.bang_facts -- Scan.lift (Scan.option OuterParse.nat) --| |
90 (Scan.lift (Scan.option OuterParse.nat) --| Method.sections modifiers >> |
91 Method.sections modifiers >> |
91 (fn opt_lim => fn ctxt => |
92 (fn (prems, n) => fn ctxt => METHOD (fn facts => |
92 SIMPLE_METHOD' (ObjectLogic.atomize_prems_tac THEN' prover_tac ctxt opt_lim))) |
93 HEADGOAL (Method.insert_tac (prems @ facts) THEN' |
|
94 ObjectLogic.atomize_prems_tac THEN' prover_tac ctxt n)))) |
|
95 "intuitionistic proof search"; |
93 "intuitionistic proof search"; |
96 |
94 |
97 end; |
95 end; |
98 |
96 |
99 end; |
97 end; |