src/HOL/List.thy
changeset 54600 ac54bc80a5cc
parent 54598 33a68b7f2736
child 54863 82acc20ded73
     1.1 --- a/src/HOL/List.thy	Wed Nov 27 10:54:44 2013 +0100
     1.2 +++ b/src/HOL/List.thy	Wed Nov 27 11:08:55 2013 +0100
     1.3 @@ -5395,7 +5395,6 @@
     1.4    Author: Andreas Lochbihler
     1.5  *}
     1.6  
     1.7 -thm not_less
     1.8  context ord begin
     1.9  
    1.10  inductive lexordp :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"