src/HOL/Library/List_lexord.thy
changeset 61076 bdc1e2f0a86a
parent 60679 ade12ef2773c
     1.1 --- a/src/HOL/Library/List_lexord.thy	Tue Sep 01 17:25:36 2015 +0200
     1.2 +++ b/src/HOL/Library/List_lexord.thy	Tue Sep 01 22:32:58 2015 +0200
     1.3 @@ -69,9 +69,9 @@
     1.4  instantiation list :: (linorder) distrib_lattice
     1.5  begin
     1.6  
     1.7 -definition "(inf \<Colon> 'a list \<Rightarrow> _) = min"
     1.8 +definition "(inf :: 'a list \<Rightarrow> _) = min"
     1.9  
    1.10 -definition "(sup \<Colon> 'a list \<Rightarrow> _) = max"
    1.11 +definition "(sup :: 'a list \<Rightarrow> _) = max"
    1.12  
    1.13  instance
    1.14    by standard (auto simp add: inf_list_def sup_list_def max_min_distrib2)
    1.15 @@ -107,15 +107,15 @@
    1.16  end
    1.17  
    1.18  lemma less_list_code [code]:
    1.19 -  "xs < ([]\<Colon>'a\<Colon>{equal, order} list) \<longleftrightarrow> False"
    1.20 -  "[] < (x\<Colon>'a\<Colon>{equal, order}) # xs \<longleftrightarrow> True"
    1.21 -  "(x\<Colon>'a\<Colon>{equal, order}) # xs < y # ys \<longleftrightarrow> x < y \<or> x = y \<and> xs < ys"
    1.22 +  "xs < ([]::'a::{equal, order} list) \<longleftrightarrow> False"
    1.23 +  "[] < (x::'a::{equal, order}) # xs \<longleftrightarrow> True"
    1.24 +  "(x::'a::{equal, order}) # xs < y # ys \<longleftrightarrow> x < y \<or> x = y \<and> xs < ys"
    1.25    by simp_all
    1.26  
    1.27  lemma less_eq_list_code [code]:
    1.28 -  "x # xs \<le> ([]\<Colon>'a\<Colon>{equal, order} list) \<longleftrightarrow> False"
    1.29 -  "[] \<le> (xs\<Colon>'a\<Colon>{equal, order} list) \<longleftrightarrow> True"
    1.30 -  "(x\<Colon>'a\<Colon>{equal, order}) # xs \<le> y # ys \<longleftrightarrow> x < y \<or> x = y \<and> xs \<le> ys"
    1.31 +  "x # xs \<le> ([]::'a::{equal, order} list) \<longleftrightarrow> False"
    1.32 +  "[] \<le> (xs::'a::{equal, order} list) \<longleftrightarrow> True"
    1.33 +  "(x::'a::{equal, order}) # xs \<le> y # ys \<longleftrightarrow> x < y \<or> x = y \<and> xs \<le> ys"
    1.34    by simp_all
    1.35  
    1.36  end