added class "default" and expansion axioms for undefined

--- a/src/HOL/HOL.thy	Tue Mar 20 15:52:37 2007 +0100
+++ b/src/HOL/HOL.thy	Tue Mar 20 15:52:38 2007 +0100
@@ -33,7 +33,6 @@
   True          :: bool
   False         :: bool
   arbitrary     :: 'a
-  undefined     :: 'a
 
   The           :: "('a => bool) => 'a"
   All           :: "('a => bool) => bool"           (binder "ALL " 10)
@@ -174,10 +173,18 @@
   "op -->"
   The
   arbitrary
-  undefined
+
+axiomatization
+  undefined :: 'a
+
+axioms
+  undefined_fun: "undefined x = undefined"
 
 
-subsubsection {* Generic algebraic operations *}
+subsubsection {* Generic classes and algebraic operations *}
+
+class default = type +
+  fixes default :: "'a"
 
 class zero = type + 
   fixes zero :: "'a"  ("\<^loc>0")