src/Tools/intuitionistic.ML
changeset 32861 105f40051387
parent 31299 0c5baf034d0e
child 33038 8f9594c31de4
equal deleted inserted replaced
32860:a4ab5d0cccd1 32861:105f40051387
    67 local
    67 local
    68 
    68 
    69 val introN = "intro";
    69 val introN = "intro";
    70 val elimN = "elim";
    70 val elimN = "elim";
    71 val destN = "dest";
    71 val destN = "dest";
    72 val ruleN = "rule";
       
    73 
    72 
    74 fun modifier name kind kind' att =
    73 fun modifier name kind kind' att =
    75   Args.$$$ name |-- (kind >> K NONE || kind' |-- OuterParse.nat --| Args.colon >> SOME)
    74   Args.$$$ name |-- (kind >> K NONE || kind' |-- OuterParse.nat --| Args.colon >> SOME)
    76     >> (pair (I: Proof.context -> Proof.context) o att);
    75     >> (pair (I: Proof.context -> Proof.context) o att);
    77 
    76