added kind attributes;

--- a/src/Pure/Isar/attrib.ML	Mon Oct 09 02:19:57 2006 +0200
+++ b/src/Pure/Isar/attrib.ML	Mon Oct 09 02:19:58 2006 +0200
@@ -34,6 +34,11 @@
     attribute * (Context.generic * Args.T list)) -> src -> attribute
   val no_args: attribute -> src -> attribute
   val add_del_args: attribute -> attribute -> src -> attribute
+  val kind: string -> src
+  val kind_theorem: src
+  val kind_lemma: src
+  val kind_corollary: src
+  val kind_internal: src
   val internal: attribute -> src
 end;
 
@@ -192,6 +197,17 @@
 fun untagged x = syntax (Scan.lift Args.name >> PureThy.untag) x;
 
 
+(* kinds *)
+
+fun kind_att x = syntax (Scan.lift Args.name >> PureThy.kind) x;
+fun kind name = Args.src (("Pure.kind", [Args.mk_string (name, Position.none)]), Position.none);
+
+val kind_theorem = kind PureThy.theoremK;
+val kind_lemma = kind PureThy.lemmaK;
+val kind_corollary = kind PureThy.corollaryK;
+val kind_internal = kind PureThy.internalK;
+
+
 (* rule composition *)
 
 val COMP_att =
@@ -263,6 +279,7 @@
  (add_attributes
    [("tagged", tagged, "tagged theorem"),
     ("untagged", untagged, "untagged theorem"),
+    ("kind", kind_att, "theorem kind"),
     ("COMP", COMP_att, "direct composition with rules (no lifting)"),
     ("THEN", THEN_att, "resolution with rule"),
     ("OF", OF_att, "rule applied to facts"),