--- a/src/HOL/Library/Fraction_Field.thy Tue Sep 01 17:25:36 2015 +0200
+++ b/src/HOL/Library/Fraction_Field.thy Tue Sep 01 22:32:58 2015 +0200
@@ -416,10 +416,10 @@
eq_fract zero_less_mult_iff mult_less_0_iff split: abs_split)
definition inf_fract_def:
- "(inf \<Colon> 'a fract \<Rightarrow> 'a fract \<Rightarrow> 'a fract) = min"
+ "(inf :: 'a fract \<Rightarrow> 'a fract \<Rightarrow> 'a fract) = min"
definition sup_fract_def:
- "(sup \<Colon> 'a fract \<Rightarrow> 'a fract \<Rightarrow> 'a fract) = max"
+ "(sup :: 'a fract \<Rightarrow> 'a fract \<Rightarrow> 'a fract) = max"
instance
by intro_classes