src/Tools/intuitionistic.ML
changeset 35625 9c818cab0dd0
parent 33554 4601372337e4
child 36960 01594f816e3a
equal deleted inserted replaced
35624:c4e29a0bb8c1 35625:9c818cab0dd0
    87 
    87 
    88 fun method_setup name =
    88 fun method_setup name =
    89   Method.setup name
    89   Method.setup name
    90     (Scan.lift (Scan.option OuterParse.nat) --| Method.sections modifiers >>
    90     (Scan.lift (Scan.option OuterParse.nat) --| Method.sections modifiers >>
    91       (fn opt_lim => fn ctxt =>
    91       (fn opt_lim => fn ctxt =>
    92         SIMPLE_METHOD' (ObjectLogic.atomize_prems_tac THEN' prover_tac ctxt opt_lim)))
    92         SIMPLE_METHOD' (Object_Logic.atomize_prems_tac THEN' prover_tac ctxt opt_lim)))
    93     "intuitionistic proof search";
    93     "intuitionistic proof search";
    94 
    94 
    95 end;
    95 end;
    96 
    96 
    97 end;
    97 end;