src/HOL/Inductive.thy
changeset 56146 8453d35e4684
parent 55604 42e4e8c2e8dc
child 58112 8081087096ad
--- a/src/HOL/Inductive.thy	Fri Mar 14 15:26:52 2014 +0100
+++ b/src/HOL/Inductive.thy	Fri Mar 14 15:41:29 2014 +0100
@@ -7,8 +7,8 @@
 theory Inductive
 imports Complete_Lattices Ctr_Sugar
 keywords
-  "inductive" "coinductive" :: thy_decl and
-  "inductive_cases" "inductive_simps" :: thy_script and "monos" and
+  "inductive" "coinductive" "inductive_cases" "inductive_simps" :: thy_decl and
+  "monos" and
   "print_inductives" :: diag and
   "rep_datatype" :: thy_goal and
   "primrec" :: thy_decl