src/Pure/Pure.thy

   and "subclass" :: thy_goal
   and "instantiation" :: thy_decl_block
   and "instance" :: thy_goal
   and "overloading" :: thy_decl_block
   and "code_datatype" :: thy_decl
-  and "theorem" "lemma" "corollary" :: thy_goal
+  and "theorem" "lemma" "corollary" "proposition" :: thy_goal
   and "schematic_goal" :: thy_goal
   and "notepad" :: thy_decl_block
   and "have" :: prf_goal % "proof"
   and "hence" :: prf_goal % "proof" == "then have"
   and "show" :: prf_asm_goal % "proof"