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")