src/Pure/more_thm.ML
changeset 31174 f1f1e9b53c81
parent 30564 deddb8a1516f
child 31177 c39994cb152a
     1.1 --- a/src/Pure/more_thm.ML	Sat May 16 15:24:35 2009 +0200
     1.2 +++ b/src/Pure/more_thm.ML	Sat May 16 20:17:59 2009 +0200
     1.3 @@ -70,6 +70,7 @@
     1.4    val assumptionK: string
     1.5    val definitionK: string
     1.6    val theoremK: string
     1.7 +  val generated_theoremK : string
     1.8    val lemmaK: string
     1.9    val corollaryK: string
    1.10    val internalK: string
    1.11 @@ -388,6 +389,7 @@
    1.12  val assumptionK = "assumption";
    1.13  val definitionK = "definition";
    1.14  val theoremK = "theorem";
    1.15 +val generated_theoremK = "generated_theoremK"
    1.16  val lemmaK = "lemma";
    1.17  val corollaryK = "corollary";
    1.18  val internalK = Markup.internalK;