src/HOL/Library/Prefix_Order.thy
changeset 63465 d7610beb98bc
parent 63117 acb6d72fc42e
     1.1 --- a/src/HOL/Library/Prefix_Order.thy	Tue Jul 12 19:12:17 2016 +0200
     1.2 +++ b/src/HOL/Library/Prefix_Order.thy	Tue Jul 12 20:03:18 2016 +0200
     1.3 @@ -11,16 +11,16 @@
     1.4  instantiation list :: (type) order
     1.5  begin
     1.6  
     1.7 -definition "(xs::'a list) \<le> ys \<equiv> prefix xs ys"
     1.8 -definition "(xs::'a list) < ys \<equiv> xs \<le> ys \<and> \<not> (ys \<le> xs)"
     1.9 +definition "xs \<le> ys \<equiv> prefix xs ys" for xs ys :: "'a list"
    1.10 +definition "xs < ys \<equiv> xs \<le> ys \<and> \<not> (ys \<le> xs)" for xs ys :: "'a list"
    1.11  
    1.12  instance
    1.13    by standard (auto simp: less_eq_list_def less_list_def)
    1.14  
    1.15  end
    1.16  
    1.17 -lemma less_list_def': "(xs::'a list) < ys \<longleftrightarrow> strict_prefix xs ys"
    1.18 -by (simp add: less_eq_list_def order.strict_iff_order prefix_order.less_le)
    1.19 +lemma less_list_def': "xs < ys \<longleftrightarrow> strict_prefix xs ys" for xs ys :: "'a list"
    1.20 +  by (simp add: less_eq_list_def order.strict_iff_order prefix_order.less_le)
    1.21  
    1.22  lemmas prefixI [intro?] = prefixI [folded less_eq_list_def]
    1.23  lemmas prefixE [elim?] = prefixE [folded less_eq_list_def]