src/HOL/List.thy
changeset 61682 f2c69a221055
parent 61668 9a51e4dfc5d9
parent 61681 ca53150406c9
child 61699 a81dc5c4d6a9
     1.1 --- a/src/HOL/List.thy	Sun Nov 15 12:45:28 2015 +0100
     1.2 +++ b/src/HOL/List.thy	Sun Nov 15 13:49:27 2015 +0100
     1.3 @@ -5573,7 +5573,12 @@
     1.4    Author: Andreas Lochbihler
     1.5  \<close>
     1.6  
     1.7 -context ord begin
     1.8 +context ord
     1.9 +begin
    1.10 +
    1.11 +context
    1.12 +  notes [[inductive_defs]]
    1.13 +begin
    1.14  
    1.15  inductive lexordp :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
    1.16  where
    1.17 @@ -5582,6 +5587,8 @@
    1.18  | Cons_eq:
    1.19    "\<lbrakk> \<not> x < y; \<not> y < x; lexordp xs ys \<rbrakk> \<Longrightarrow> lexordp (x # xs) (y # ys)"
    1.20  
    1.21 +end
    1.22 +
    1.23  lemma lexordp_simps [simp]:
    1.24    "lexordp [] ys = (ys \<noteq> [])"
    1.25    "lexordp xs [] = False"
    1.26 @@ -5636,7 +5643,8 @@
    1.27  lemma lexord_code [code, code_unfold]: "lexordp = ord.lexordp less"
    1.28  unfolding lexordp_def ord.lexordp_def ..
    1.29  
    1.30 -context order begin
    1.31 +context order
    1.32 +begin
    1.33  
    1.34  lemma lexordp_antisym:
    1.35    assumes "lexordp xs ys" "lexordp ys xs"