src/HOL/HOL.thy
changeset 14223 0ee05eef881b
parent 14208 144f45277d5a
child 14248 399a3290936c
     1.1 --- a/src/HOL/HOL.thy	Wed Oct 08 16:02:54 2003 +0200
     1.2 +++ b/src/HOL/HOL.thy	Thu Oct 09 18:13:32 2003 +0200
     1.3 @@ -146,10 +146,11 @@
     1.4    Let_def:      "Let s f == f(s)"
     1.5    if_def:       "If P x y == THE z::'a. (P=True --> z=x) & (P=False --> z=y)"
     1.6  
     1.7 -  arbitrary_def:  "False ==> arbitrary == (THE x. False)"
     1.8 -    -- {* @{term arbitrary} is completely unspecified, but is made to appear as a
     1.9 -    definition syntactically *}
    1.10 -
    1.11 +finalconsts
    1.12 +  "op ="
    1.13 +  "op -->"
    1.14 +  The
    1.15 +  arbitrary
    1.16  
    1.17  subsubsection {* Generic algebraic operations *}
    1.18