src/HOL/List.thy
changeset 62100 7a5754afe170
parent 62090 db9996a84166
parent 62093 bd73a2279fcd
child 62175 8ffc4d0e652d
     1.1 --- a/src/HOL/List.thy	Fri Jan 08 16:36:41 2016 +0100
     1.2 +++ b/src/HOL/List.thy	Fri Jan 08 16:37:56 2016 +0100
     1.3 @@ -5652,7 +5652,7 @@
     1.4  begin
     1.5  
     1.6  context
     1.7 -  notes [[inductive_defs]]
     1.8 +  notes [[inductive_internals]]
     1.9  begin
    1.10  
    1.11  inductive lexordp :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"