src/HOL/Inductive.thy
changeset 46950 d0181abdbdac
parent 46947 b8c7eb0c2f89
child 48357 828ace4f75ab
--- a/src/HOL/Inductive.thy	Thu Mar 15 20:07:00 2012 +0100
+++ b/src/HOL/Inductive.thy	Thu Mar 15 22:08:53 2012 +0100
@@ -6,7 +6,11 @@
 
 theory Inductive 
 imports Complete_Lattices
-keywords "monos"
+keywords
+  "inductive" "coinductive" :: thy_decl and
+  "inductive_cases" "inductive_simps" :: thy_script and "monos" and
+  "rep_datatype" :: thy_goal and
+  "primrec" :: thy_decl
 uses
   "Tools/dseq.ML"
   ("Tools/inductive.ML")