src/HOL/Inductive.thy
changeset 46950 d0181abdbdac
parent 46947 b8c7eb0c2f89
child 48357 828ace4f75ab
     1.1 --- a/src/HOL/Inductive.thy	Thu Mar 15 20:07:00 2012 +0100
     1.2 +++ b/src/HOL/Inductive.thy	Thu Mar 15 22:08:53 2012 +0100
     1.3 @@ -6,7 +6,11 @@
     1.4  
     1.5  theory Inductive 
     1.6  imports Complete_Lattices
     1.7 -keywords "monos"
     1.8 +keywords
     1.9 +  "inductive" "coinductive" :: thy_decl and
    1.10 +  "inductive_cases" "inductive_simps" :: thy_script and "monos" and
    1.11 +  "rep_datatype" :: thy_goal and
    1.12 +  "primrec" :: thy_decl
    1.13  uses
    1.14    "Tools/dseq.ML"
    1.15    ("Tools/inductive.ML")