changeset 42440 | 5e7a7343ab11 |
parent 42375 | 774df7c59508 |
child 42473 | aca720fb3936 |
--- a/src/Pure/more_thm.ML Wed Apr 20 22:57:29 2011 +0200 +++ b/src/Pure/more_thm.ML Thu Apr 21 12:56:27 2011 +0200 @@ -87,7 +87,6 @@ val has_name_hint: thm -> bool val get_name_hint: thm -> string val put_name_hint: string -> thm -> thm - val definitionK: string val theoremK: string val lemmaK: string val corollaryK: string @@ -450,7 +449,6 @@ (* theorem kinds *) -val definitionK = "definition"; val theoremK = "theorem"; val lemmaK = "lemma"; val corollaryK = "corollary";