src/Pure/Isar/isar_syn.ML

           Thm.theoremK NONE (K I) a includes elems concl)));
 
 val _ = theorem @{command_keyword theorem} false "theorem";
 val _ = theorem @{command_keyword lemma} false "lemma";
 val _ = theorem @{command_keyword corollary} false "corollary";
+val _ = theorem @{command_keyword proposition} false "proposition";
 val _ = theorem @{command_keyword schematic_goal} true "schematic goal";
 
 
 val structured_statement =
   Parse_Spec.statement -- Parse_Spec.cond_statement -- Parse.for_fixes