changeset 55973 | ac54bc80a5cc |
parent 55971 | 33a68b7f2736 |
child 56205 | 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"