1.1 --- a/src/HOL/HOL.thy	Tue Oct 16 23:12:38 2007 +0200
     1.2 +++ b/src/HOL/HOL.thy	Tue Oct 16 23:12:45 2007 +0200
     1.3 @@ -208,75 +208,55 @@
     1.4    fixes default :: 'a
     1.5  
     1.6  class zero = type + 
     1.7 -  fixes zero :: 'a  ("\<^loc>0")
     1.8 +  fixes zero :: 'a  ("0")
     1.9  
    1.10  class one = type +
    1.11 -  fixes one  :: 'a  ("\<^loc>1")
    1.12 +  fixes one  :: 'a  ("1")
    1.13  
    1.14  hide (open) const zero one
    1.15  
    1.16  class plus = type +
    1.17 -  fixes plus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "\<^loc>+" 65)
    1.18 +  fixes plus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "+" 65)
    1.19  
    1.20  class minus = type +
    1.21 -  fixes uminus :: "'a \<Rightarrow> 'a" 
    1.22 -    and minus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "\<^loc>-" 65)
    1.23 +  fixes uminus :: "'a \<Rightarrow> 'a"  ("- _" [81] 80)
    1.24 +    and minus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "-" 65)
    1.25  
    1.26  class times = type +
    1.27 -  fixes times :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "\<^loc>*" 70)
    1.28 +  fixes times :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "*" 70)
    1.29  
    1.30  class inverse = type +
    1.31    fixes inverse :: "'a \<Rightarrow> 'a"
    1.32 -    and divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "\<^loc>'/" 70)
    1.33 +    and divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "'/" 70)
    1.34  
    1.35  class abs = type +
    1.36    fixes abs :: "'a \<Rightarrow> 'a"
    1.37  
    1.38 -class sgn = type +
    1.39 -  fixes sgn :: "'a \<Rightarrow> 'a"
    1.40 -
    1.41 -notation
    1.42 -  uminus  ("- _" [81] 80)
    1.43 -
    1.44  notation (xsymbols)
    1.45    abs  ("\<bar>_\<bar>")
    1.46  notation (HTML output)
    1.47    abs  ("\<bar>_\<bar>")
    1.48  
    1.49 +class sgn = type +
    1.50 +  fixes sgn :: "'a \<Rightarrow> 'a"
    1.51 +
    1.52  class ord = type +
    1.53    fixes less_eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
    1.54      and less :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
    1.55  begin
    1.56  
    1.57 -notation
    1.58 -  less_eq  ("op \<^loc><=") and
    1.59 -  less_eq  ("(_/ \<^loc><= _)" [51, 51] 50) and
    1.60 -  less  ("op \<^loc><") and
    1.61 -  less  ("(_/ \<^loc>< _)"  [51, 51] 50)
    1.62 -  
    1.63 -notation (xsymbols)
    1.64 -  less_eq  ("op \<^loc>\<le>") and
    1.65 -  less_eq  ("(_/ \<^loc>\<le> _)"  [51, 51] 50)
    1.66 -
    1.67 -notation (HTML output)
    1.68 -  less_eq  ("op \<^loc>\<le>") and
    1.69 -  less_eq  ("(_/ \<^loc>\<le> _)"  [51, 51] 50)
    1.70 +abbreviation (input)
    1.71 +  greater_eq  (infix ">=" 50) where
    1.72 +  "x >= y \<equiv> less_eq y x"
    1.73  
    1.74  abbreviation (input)
    1.75 -  greater_eq  (infix "\<^loc>>=" 50) where
    1.76 -  "x \<^loc>>= y \<equiv> y \<^loc><= x"
    1.77 -
    1.78 -notation (input)
    1.79 -  greater_eq  (infix "\<^loc>\<ge>" 50)
    1.80 -
    1.81 -abbreviation (input)
    1.82 -  greater  (infix "\<^loc>>" 50) where
    1.83 -  "x \<^loc>> y \<equiv> y \<^loc>< x"
    1.84 +  greater  (infix ">" 50) where
    1.85 +  "x > y \<equiv> less y x"
    1.86  
    1.87  definition
    1.88 -  Least :: "('a \<Rightarrow> bool) \<Rightarrow> 'a" (binder "\<^loc>LEAST " 10)
    1.89 +  Least :: "('a \<Rightarrow> bool) \<Rightarrow> 'a" (binder "LEAST " 10)
    1.90  where
    1.91 -  "Least P == (THE x. P x \<and> (\<forall>y. P y \<longrightarrow> x \<^loc>\<le> y))"
    1.92 +  "Least P == (THE x. P x \<and> (\<forall>y. P y \<longrightarrow> less_eq x y))"
    1.93  
    1.94  end
    1.95