diff -r 5471709833a4 -r d3cbf79769b9 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Mon Oct 08 08:04:26 2007 +0200
+++ b/src/HOL/HOL.thy	Mon Oct 08 08:04:28 2007 +0200
@@ -22,13 +22,13 @@
   "~~/src/Provers/eqsubst.ML"
   "~~/src/Provers/quantifier1.ML"
   ("simpdata.ML")
+  "~~/src/Tools/induct.ML"
   "~~/src/Tools/code/code_name.ML"
   "~~/src/Tools/code/code_funcgr.ML"
   "~~/src/Tools/code/code_thingol.ML"
   "~~/src/Tools/code/code_target.ML"
   "~~/src/Tools/code/code_package.ML"
   "~~/src/Tools/nbe.ML"
-  "~~/src/Tools/induct.ML"
 begin
 
 subsection {* Primitive logic *}
@@ -205,13 +205,13 @@
 subsubsection {* Generic classes and algebraic operations *}
 
 class default = type +
-  fixes default :: "'a"
+  fixes default :: 'a
 
 class zero = type + 
-  fixes zero :: "'a"  ("\<^loc>0")
+  fixes zero :: 'a  ("\<^loc>0")
 
 class one = type +
-  fixes one  :: "'a"  ("\<^loc>1")
+  fixes one  :: 'a  ("\<^loc>1")
 
 hide (open) const zero one
 
@@ -295,11 +295,6 @@
   less_eq  ("(_/ \<le> _)"  [51, 51] 50)
 
 notation (input)
-  greater  (infix ">" 50)
-
-notation (input)
-  greater_eq  (infix ">=" 50)
-and
   greater_eq  (infix "\<ge>" 50)
 
 syntax