changeset 55534 | b18bdcbda41b |
parent 54615 | 62fb5af93fe2 |
child 55575 | a5e33e18fb5c |
--- a/src/HOL/Inductive.thy Mon Feb 17 13:31:42 2014 +0100 +++ b/src/HOL/Inductive.thy Mon Feb 17 13:31:42 2014 +0100 @@ -11,7 +11,7 @@ "inductive_cases" "inductive_simps" :: thy_script and "monos" and "print_inductives" :: diag and "rep_datatype" :: thy_goal and - "primrec" :: thy_decl + "old_primrec" :: thy_decl begin subsection {* Least and greatest fixed points *}