src/HOL/Library/Char_ord.thy
changeset 25502 9200b36280c0
parent 23394 474ff28210c0
child 25764 878c37886eed
     1.1 --- a/src/HOL/Library/Char_ord.thy	Thu Nov 29 07:55:46 2007 +0100
     1.2 +++ b/src/HOL/Library/Char_ord.thy	Thu Nov 29 17:08:26 2007 +0100
     1.3 @@ -39,8 +39,8 @@
     1.4  qed
     1.5  
     1.6  instance nibble :: distrib_lattice
     1.7 -    "inf \<equiv> min"
     1.8 -    "sup \<equiv> max"
     1.9 +  "(inf \<Colon> nibble \<Rightarrow> _) = min"
    1.10 +  "(sup \<Colon> nibble \<Rightarrow> _) = max"
    1.11    by default (auto simp add:
    1.12      inf_nibble_def sup_nibble_def min_max.sup_inf_distrib1)
    1.13  
    1.14 @@ -54,8 +54,8 @@
    1.15  lemmas [code func del] = char_less_eq_def char_less_def
    1.16  
    1.17  instance char :: distrib_lattice
    1.18 -    "inf \<equiv> min"
    1.19 -    "sup \<equiv> max"
    1.20 +  "(inf \<Colon> char \<Rightarrow> _) = min"
    1.21 +  "(sup \<Colon> char \<Rightarrow> _) = max"
    1.22    by default (auto simp add:
    1.23      inf_char_def sup_char_def min_max.sup_inf_distrib1)
    1.24