src/HOL/Library/List_Prefix.thy
changeset 23394 474ff28210c0
parent 23254 99644a53f16d
child 25299 c3542f70b0fd
     1.1 --- a/src/HOL/Library/List_Prefix.thy	Thu Jun 14 23:04:36 2007 +0200
     1.2 +++ b/src/HOL/Library/List_Prefix.thy	Thu Jun 14 23:04:39 2007 +0200
     1.3 @@ -26,7 +26,7 @@
     1.4  lemma prefixE [elim?]:
     1.5    assumes "xs \<le> ys"
     1.6    obtains zs where "ys = xs @ zs"
     1.7 -  using prems unfolding prefix_def by blast
     1.8 +  using assms unfolding prefix_def by blast
     1.9  
    1.10  lemma strict_prefixI' [intro?]: "ys = xs @ z # zs ==> xs < ys"
    1.11    unfolding strict_prefix_def prefix_def by blast
    1.12 @@ -47,7 +47,7 @@
    1.13    fixes xs ys :: "'a list"
    1.14    assumes "xs < ys"
    1.15    obtains "xs \<le> ys" and "xs \<noteq> ys"
    1.16 -  using prems unfolding strict_prefix_def by blast
    1.17 +  using assms unfolding strict_prefix_def by blast
    1.18  
    1.19  
    1.20  subsection {* Basic properties of prefixes *}
    1.21 @@ -168,7 +168,7 @@
    1.22  lemma parallelE [elim]:
    1.23    assumes "xs \<parallel> ys"
    1.24    obtains "\<not> xs \<le> ys \<and> \<not> ys \<le> xs"
    1.25 -  using prems unfolding parallel_def by blast
    1.26 +  using assms unfolding parallel_def by blast
    1.27  
    1.28  theorem prefix_cases:
    1.29    obtains "xs \<le> ys" | "ys < xs" | "xs \<parallel> ys"
    1.30 @@ -227,7 +227,7 @@
    1.31  lemma postfixE [elim?]:
    1.32    assumes "xs >>= ys"
    1.33    obtains zs where "xs = zs @ ys"
    1.34 -  using prems unfolding postfix_def by blast
    1.35 +  using assms unfolding postfix_def by blast
    1.36  
    1.37  lemma postfix_refl [iff]: "xs >>= xs"
    1.38    by (auto simp add: postfix_def)