diff -r d54ee0cad2ab -r cfc83ad52571 src/Pure/Pure.thy --- a/src/Pure/Pure.thy Mon Feb 25 12:52:27 2013 +0100 +++ b/src/Pure/Pure.thy Mon Feb 25 13:29:19 2013 +0100 @@ -50,7 +50,7 @@ and "overloading" :: thy_decl and "code_datatype" :: thy_decl and "theorem" "lemma" "corollary" :: thy_goal - and "schematic_theorem" "schematic_lemma" "schematic_corollary" :: thy_schematic_goal + and "schematic_theorem" "schematic_lemma" "schematic_corollary" :: thy_goal and "notepad" :: thy_decl and "have" :: prf_goal % "proof" and "hence" :: prf_goal % "proof" == "then have"