src/Tools/intuitionistic.ML
changeset 30510 4120fc59dd85
parent 30165 6ee87f67d9cd
child 31299 0c5baf034d0e
equal deleted inserted replaced
30509:e19d5b459a61 30510:4120fc59dd85
    84   modifier introN Args.colon (Scan.succeed ()) ContextRules.intro,
    84   modifier introN Args.colon (Scan.succeed ()) ContextRules.intro,
    85   Args.del -- Args.colon >> K (I, ContextRules.rule_del)];
    85   Args.del -- Args.colon >> K (I, ContextRules.rule_del)];
    86 
    86 
    87 val method =
    87 val method =
    88   Method.bang_sectioned_args' modifiers (Scan.lift (Scan.option OuterParse.nat))
    88   Method.bang_sectioned_args' modifiers (Scan.lift (Scan.option OuterParse.nat))
    89     (fn n => fn prems => fn ctxt => Method.METHOD (fn facts =>
    89     (fn n => fn prems => fn ctxt => METHOD (fn facts =>
    90       HEADGOAL (Method.insert_tac (prems @ facts) THEN'
    90       HEADGOAL (Method.insert_tac (prems @ facts) THEN'
    91       ObjectLogic.atomize_prems_tac THEN' prover_tac ctxt n)));
    91       ObjectLogic.atomize_prems_tac THEN' prover_tac ctxt n)));
    92 
    92 
    93 in
    93 in
    94 
    94