src/HOL/HOL.thy
changeset 31804 627d142fce19
parent 31299 0c5baf034d0e
child 31902 862ae16a799d
equal deleted inserted replaced
31799:294b955d0e80 31804:627d142fce19
   195   "op -->"
   195   "op -->"
   196   The
   196   The
   197 
   197 
   198 axiomatization
   198 axiomatization
   199   undefined :: 'a
   199   undefined :: 'a
   200 
       
   201 abbreviation (input)
       
   202   "arbitrary \<equiv> undefined"
       
   203 
   200 
   204 
   201 
   205 subsubsection {* Generic classes and algebraic operations *}
   202 subsubsection {* Generic classes and algebraic operations *}
   206 
   203 
   207 class default =
   204 class default =