src/Pure/more_thm.ML
changeset 22378 8e02a61b401f
parent 22362 6470ce514b6e
child 22682 92448396c9d9
equal deleted inserted replaced
22377:61610b1beedf 22378:8e02a61b401f
    74 val lemmaK = "lemma";
    74 val lemmaK = "lemma";
    75 val corollaryK = "corollary";
    75 val corollaryK = "corollary";
    76 val internalK = "internal";
    76 val internalK = "internal";
    77 
    77 
    78 
    78 
    79 
       
    80 (* attributes *)
    79 (* attributes *)
    81 
    80 
    82 fun rule_attribute f (x, th) = (x, f x th);
    81 fun rule_attribute f (x, th) = (x, f x th);
    83 fun declaration_attribute f (x, th) = (f th x, th);
    82 fun declaration_attribute f (x, th) = (f th x, th);
    84 
    83