src/HOL/Library/List_lexord.thy

 
 theory List_lexord
 imports List
 begin
 
-instance list :: (ord) ord
+instantiation list :: (ord) ord
+begin
+
+definition
   list_less_def [code func del]: "(xs::('a::ord) list) < ys \<longleftrightarrow> (xs, ys) \<in> lexord {(u,v). u < v}"
-  list_le_def [code func del]: "(xs::('a::ord) list) \<le> ys \<longleftrightarrow> (xs < ys \<or> xs = ys)" ..
+
+definition
+  list_le_def [code func del]: "(xs::('a::ord) list) \<le> ys \<longleftrightarrow> (xs < ys \<or> xs = ys)"
+
+instance ..
+
+end
 
 instance list :: (order) order
   apply (intro_classes, unfold list_less_def list_le_def)
   apply safe
   apply (rule_tac r1 = "{(a::'a,b). a < b}" in lexord_irreflexive [THEN notE])

   apply (cut_tac x = x and y = y and  r = "{(a,b). a < b}"  in lexord_linear)
    apply force
   apply simp
   done
 
-instance list :: (linorder) distrib_lattice
+instantiation list :: (linorder) distrib_lattice
+begin
+
+definition
   [code func del]: "(inf \<Colon> 'a list \<Rightarrow> _) = min"
+
+definition
   [code func del]: "(sup \<Colon> 'a list \<Rightarrow> _) = max"
+
+instance
   by intro_classes
     (auto simp add: inf_list_def sup_list_def min_max.sup_inf_distrib1)
+
+end
 
 lemma not_less_Nil [simp]: "\<not> (x < [])"
   by (unfold list_less_def) simp
 
 lemma Nil_less_Cons [simp]: "[] < a # x"