--- a/src/HOL/HOL.thy Mon Jun 22 17:13:09 1998 +0200
+++ b/src/HOL/HOL.thy Mon Jun 22 17:26:46 1998 +0200
@@ -178,11 +178,13 @@
True_or_False "(P=True) | (P=False)"
defs
- (* Misc Definitions *)
-
+ (*misc definitions*)
Let_def "Let s f == f(s)"
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)"
+
+ (*arbitrary is completely unspecified, but is made to appear as a
+ definition syntactically*)
arbitrary_def "False ==> arbitrary == (@x. False)"