src/HOL/Library/List_Prefix.thy
changeset 10512 d34192966cd8
parent 10408 d8b3613158b1
child 10870 9444e3cf37e1
     1.1 --- a/src/HOL/Library/List_Prefix.thy	Wed Nov 22 21:41:39 2000 +0100
     1.2 +++ b/src/HOL/Library/List_Prefix.thy	Wed Nov 22 21:47:04 2000 +0100
     1.3 @@ -131,9 +131,9 @@
     1.4  
     1.5  theorem prefix_cases:
     1.6    "(xs \<le> ys ==> C) ==>
     1.7 -    (ys \<le> xs ==> C) ==>
     1.8 +    (ys < xs ==> C) ==>
     1.9      (xs \<parallel> ys ==> C) ==> C"
    1.10 -  by (unfold parallel_def) blast
    1.11 +  by (unfold parallel_def strict_prefix_def) blast
    1.12  
    1.13  theorem parallel_decomp:
    1.14    "xs \<parallel> ys ==> \<exists>as b bs c cs. b \<noteq> c \<and> xs = as @ b # bs \<and> ys = as @ c # cs"
    1.15 @@ -164,7 +164,7 @@
    1.16        ultimately show ?thesis by blast
    1.17      qed
    1.18    next
    1.19 -    assume "ys \<le> xs" hence "ys \<le> xs @ [x]" by simp
    1.20 +    assume "ys < xs" hence "ys \<le> xs @ [x]" by (simp add: strict_prefix_def)
    1.21      with asm have False by blast
    1.22      thus ?thesis ..
    1.23    next