1.1 --- a/src/HOL/HOL.thy	Tue Mar 20 15:52:37 2007 +0100
     1.2 +++ b/src/HOL/HOL.thy	Tue Mar 20 15:52:38 2007 +0100
     1.3 @@ -33,7 +33,6 @@
     1.4    True          :: bool
     1.5    False         :: bool
     1.6    arbitrary     :: 'a
     1.7 -  undefined     :: 'a
     1.8  
     1.9    The           :: "('a => bool) => 'a"
    1.10    All           :: "('a => bool) => bool"           (binder "ALL " 10)
    1.11 @@ -174,10 +173,18 @@
    1.12    "op -->"
    1.13    The
    1.14    arbitrary
    1.15 -  undefined
    1.16  
    1.17 +axiomatization
    1.18 +  undefined :: 'a
    1.19  
    1.20 -subsubsection {* Generic algebraic operations *}
    1.21 +axioms
    1.22 +  undefined_fun: "undefined x = undefined"
    1.23 +
    1.24 +
    1.25 +subsubsection {* Generic classes and algebraic operations *}
    1.26 +
    1.27 +class default = type +
    1.28 +  fixes default :: "'a"
    1.29  
    1.30  class zero = type + 
    1.31    fixes zero :: "'a"  ("\<^loc>0")