# HG changeset patch
# User haftmann
# Date 1224863314 -7200
# Node ID 5de9fc98ad961b6c9be280580a7dd724f73de890
# Parent  e8664643f54391cf5297a454565913675766c114
"arbitrary" merely abbreviates undefined

diff -r e8664643f543 -r 5de9fc98ad96 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Fri Oct 24 17:48:33 2008 +0200
+++ b/src/HOL/HOL.thy	Fri Oct 24 17:48:34 2008 +0200
@@ -202,11 +202,8 @@
 axiomatization
   undefined :: 'a
 
-consts
-  arbitrary :: 'a
-
-finalconsts
-  arbitrary
+abbreviation (input)
+  "arbitrary \<equiv> undefined"
 
 
 subsubsection {* Generic classes and algebraic operations *}