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