# HG changeset patch # User wenzelm # Date 881338778 -3600 # Node ID 8755cdbbf6b36e112581104cb449d2c1fbd50303 # Parent 162abcd128a18ab40cf99853db56c8574b6e1cb0 improved arbitrary_def: we now really don't know nothing about it! diff -r 162abcd128a1 -r 8755cdbbf6b3 src/HOL/HOL.thy --- a/src/HOL/HOL.thy Fri Dec 05 17:16:22 1997 +0100 +++ b/src/HOL/HOL.thy Fri Dec 05 17:19:38 1997 +0100 @@ -183,6 +183,7 @@ 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_def "False ==> arbitrary == (@x. False)" end