# HG changeset patch
# User haftmann
# Date 1174402358 -3600
# Node ID 79c2724c36b5c670720f36b3f9330b6c6bdef49f
# Parent  b20bc8029edb5f13d2b50ea1d6e1d0e3ab37fba1
added class "default" and expansion axioms for undefined

diff -r b20bc8029edb -r 79c2724c36b5 src/HOL/HOL.thy
--- 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")