src/HOL/Library/Char_ord.thy
changeset 61076 bdc1e2f0a86a
parent 60679 ade12ef2773c
child 62597 b3f2b8c906a6
     1.1 --- a/src/HOL/Library/Char_ord.thy	Tue Sep 01 17:25:36 2015 +0200
     1.2 +++ b/src/HOL/Library/Char_ord.thy	Tue Sep 01 22:32:58 2015 +0200
     1.3 @@ -22,8 +22,8 @@
     1.4  instantiation nibble :: distrib_lattice
     1.5  begin
     1.6  
     1.7 -definition "(inf \<Colon> nibble \<Rightarrow> _) = min"
     1.8 -definition "(sup \<Colon> nibble \<Rightarrow> _) = max"
     1.9 +definition "(inf :: nibble \<Rightarrow> _) = min"
    1.10 +definition "(sup :: nibble \<Rightarrow> _) = max"
    1.11  
    1.12  instance
    1.13    by standard (auto simp add: inf_nibble_def sup_nibble_def max_min_distrib2)
    1.14 @@ -74,8 +74,8 @@
    1.15  instantiation char :: distrib_lattice
    1.16  begin
    1.17  
    1.18 -definition "(inf \<Colon> char \<Rightarrow> _) = min"
    1.19 -definition "(sup \<Colon> char \<Rightarrow> _) = max"
    1.20 +definition "(inf :: char \<Rightarrow> _) = min"
    1.21 +definition "(sup :: char \<Rightarrow> _) = max"
    1.22  
    1.23  instance
    1.24    by standard (auto simp add: inf_char_def sup_char_def max_min_distrib2)