--- a/src/HOL/HOL.thy Fri May 23 14:52:45 1997 +0200
+++ b/src/HOL/HOL.thy Fri May 23 18:17:53 1997 +0200
@@ -176,6 +176,9 @@
o_def "(f::'b=>'c) o g == (%(x::'a). f(g(x)))"
if_def "If P x y == @z::'a. (P=True --> z=x) & (P=False --> z=y)"
+constdefs arbitrary :: 'a
+ "arbitrary == @x.False"
+
end