src/HOL/HOL.thy
changeset 31804 627d142fce19
parent 31299 0c5baf034d0e
child 31902 862ae16a799d
--- a/src/HOL/HOL.thy	Thu Jun 25 07:34:30 2009 +0200
+++ b/src/HOL/HOL.thy	Thu Jun 25 14:59:29 2009 +0200
@@ -198,9 +198,6 @@
 axiomatization
   undefined :: 'a
 
-abbreviation (input)
-  "arbitrary \<equiv> undefined"
-
 
 subsubsection {* Generic classes and algebraic operations *}