src/HOL/HOL.thy

   fixes inverse :: "'a \<Rightarrow> 'a"
     and divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "\<^loc>'/" 70)
 
 class abs = type +
   fixes abs :: "'a \<Rightarrow> 'a"
+
+class sgn = type +
+  fixes sgn :: "'a \<Rightarrow> 'a"
 
 notation
   uminus  ("- _" [81] 80)
 
 notation (xsymbols)