--- a/src/HOL/List.thy Sat Nov 14 18:37:49 2015 +0100
+++ b/src/HOL/List.thy Sun Nov 15 12:39:51 2015 +0100
@@ -5573,7 +5573,12 @@
Author: Andreas Lochbihler
\<close>
-context ord begin
+context ord
+begin
+
+context
+ notes [[inductive_defs]]
+begin
inductive lexordp :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
where
@@ -5582,6 +5587,8 @@
| Cons_eq:
"\<lbrakk> \<not> x < y; \<not> y < x; lexordp xs ys \<rbrakk> \<Longrightarrow> lexordp (x # xs) (y # ys)"
+end
+
lemma lexordp_simps [simp]:
"lexordp [] ys = (ys \<noteq> [])"
"lexordp xs [] = False"
@@ -5636,7 +5643,8 @@
lemma lexord_code [code, code_unfold]: "lexordp = ord.lexordp less"
unfolding lexordp_def ord.lexordp_def ..
-context order begin
+context order
+begin
lemma lexordp_antisym:
assumes "lexordp xs ys" "lexordp ys xs"