src/Pure/more_thm.ML
changeset 31174 f1f1e9b53c81
parent 30564 deddb8a1516f
child 31177 c39994cb152a
--- a/src/Pure/more_thm.ML	Sat May 16 15:24:35 2009 +0200
+++ b/src/Pure/more_thm.ML	Sat May 16 20:17:59 2009 +0200
@@ -70,6 +70,7 @@
   val assumptionK: string
   val definitionK: string
   val theoremK: string
+  val generated_theoremK : string
   val lemmaK: string
   val corollaryK: string
   val internalK: string
@@ -388,6 +389,7 @@
 val assumptionK = "assumption";
 val definitionK = "definition";
 val theoremK = "theorem";
+val generated_theoremK = "generated_theoremK"
 val lemmaK = "lemma";
 val corollaryK = "corollary";
 val internalK = Markup.internalK;