src/Tools/intuitionistic.ML
changeset 64556 851ae0e7b09c
parent 59164 ff40c53d1af9
equal deleted inserted replaced
64555:628b271c5b8b 64556:851ae0e7b09c
    76 fun modifier name kind kind' att pos =
    76 fun modifier name kind kind' att pos =
    77   Args.$$$ name |-- (kind >> K NONE || kind' |-- Parse.nat --| Args.colon >> SOME)
    77   Args.$$$ name |-- (kind >> K NONE || kind' |-- Parse.nat --| Args.colon >> SOME)
    78     >> (fn arg => Method.modifier (att arg) pos);
    78     >> (fn arg => Method.modifier (att arg) pos);
    79 
    79 
    80 val modifiers =
    80 val modifiers =
    81  [modifier destN Args.bang_colon Args.bang Context_Rules.dest_bang @{here},
    81  [modifier destN Args.bang_colon Args.bang Context_Rules.dest_bang \<^here>,
    82   modifier destN Args.colon (Scan.succeed ()) Context_Rules.dest @{here},
    82   modifier destN Args.colon (Scan.succeed ()) Context_Rules.dest \<^here>,
    83   modifier elimN Args.bang_colon Args.bang Context_Rules.elim_bang @{here},
    83   modifier elimN Args.bang_colon Args.bang Context_Rules.elim_bang \<^here>,
    84   modifier elimN Args.colon (Scan.succeed ()) Context_Rules.elim @{here},
    84   modifier elimN Args.colon (Scan.succeed ()) Context_Rules.elim \<^here>,
    85   modifier introN Args.bang_colon Args.bang Context_Rules.intro_bang @{here},
    85   modifier introN Args.bang_colon Args.bang Context_Rules.intro_bang \<^here>,
    86   modifier introN Args.colon (Scan.succeed ()) Context_Rules.intro @{here},
    86   modifier introN Args.colon (Scan.succeed ()) Context_Rules.intro \<^here>,
    87   Args.del -- Args.colon >> K (Method.modifier Context_Rules.rule_del @{here})];
    87   Args.del -- Args.colon >> K (Method.modifier Context_Rules.rule_del \<^here>)];
    88 
    88 
    89 in
    89 in
    90 
    90 
    91 fun method_setup name =
    91 fun method_setup name =
    92   Method.setup name
    92   Method.setup name