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