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