src/HOL/Datatype.thy
changeset 46950 d0181abdbdac
parent 45694 4a8743618257
child 47488 be6dd389639d
--- a/src/HOL/Datatype.thy	Thu Mar 15 20:07:00 2012 +0100
+++ b/src/HOL/Datatype.thy	Thu Mar 15 22:08:53 2012 +0100
@@ -7,6 +7,7 @@
 
 theory Datatype
 imports Product_Type Sum_Type Nat
+keywords "datatype" :: thy_decl
 uses
   ("Tools/Datatype/datatype.ML")
   ("Tools/inductive_realizer.ML")