src/HOL/Library/Char_ord.thy
changeset 54863 82acc20ded73
parent 54595 a2eeeb335a48
child 55426 90f2ceed2828
     1.1 --- a/src/HOL/Library/Char_ord.thy	Wed Dec 25 17:39:06 2013 +0100
     1.2 +++ b/src/HOL/Library/Char_ord.thy	Wed Dec 25 17:39:06 2013 +0100
     1.3 @@ -32,7 +32,7 @@
     1.4    "(sup \<Colon> nibble \<Rightarrow> _) = max"
     1.5  
     1.6  instance proof
     1.7 -qed (auto simp add: inf_nibble_def sup_nibble_def min_max.sup_inf_distrib1)
     1.8 +qed (auto simp add: inf_nibble_def sup_nibble_def max_min_distrib2)
     1.9  
    1.10  end
    1.11  
    1.12 @@ -90,7 +90,7 @@
    1.13    "(sup \<Colon> char \<Rightarrow> _) = max"
    1.14  
    1.15  instance proof
    1.16 -qed (auto simp add: inf_char_def sup_char_def min_max.sup_inf_distrib1)
    1.17 +qed (auto simp add: inf_char_def sup_char_def max_min_distrib2)
    1.18  
    1.19  end
    1.20