src/HOL/HOL.thy

--- a/src/HOL/HOL.thy	Wed Oct 08 16:02:54 2003 +0200
+++ b/src/HOL/HOL.thy	Thu Oct 09 18:13:32 2003 +0200
@@ -146,10 +146,11 @@
   Let_def:      "Let s f == f(s)"
   if_def:       "If P x y == THE z::'a. (P=True --> z=x) & (P=False --> z=y)"
 
-  arbitrary_def:  "False ==> arbitrary == (THE x. False)"
-    -- {* @{term arbitrary} is completely unspecified, but is made to appear as a
-    definition syntactically *}
-
+finalconsts
+  "op ="
+  "op -->"
+  The
+  arbitrary
 
 subsubsection {* Generic algebraic operations *}