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