# HG changeset patch
# User Andreas Lochbihler
# Date 1385546935 -3600
# Node ID ac54bc80a5cc15f5803d630f18b82a8238e32db3
# Parent  17d76426c7da14ed281f7998b98a58e3c32ebd54
remove junk

diff -r 17d76426c7da -r ac54bc80a5cc src/HOL/List.thy
--- a/src/HOL/List.thy	Wed Nov 27 10:54:44 2013 +0100
+++ b/src/HOL/List.thy	Wed Nov 27 11:08:55 2013 +0100
@@ -5395,7 +5395,6 @@
   Author: Andreas Lochbihler
 *}
 
-thm not_less
 context ord begin
 
 inductive lexordp :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"