improved arbitrary_def: we now really don't know nothing about it!
authorwenzelm
Fri Dec 05 17:19:38 1997 +0100 (1997-12-05)
changeset 43718755cdbbf6b3
parent 4370 162abcd128a1
child 4372 b9852572af0f
improved arbitrary_def: we now really don't know nothing about it!
src/HOL/HOL.thy
     1.1 --- a/src/HOL/HOL.thy	Fri Dec 05 17:16:22 1997 +0100
     1.2 +++ b/src/HOL/HOL.thy	Fri Dec 05 17:19:38 1997 +0100
     1.3 @@ -183,6 +183,7 @@
     1.4    Let_def       "Let s f == f(s)"
     1.5    o_def         "(f::'b=>'c) o g == (%(x::'a). f(g(x)))"
     1.6    if_def        "If P x y == @z::'a. (P=True --> z=x) & (P=False --> z=y)"
     1.7 +  arbitrary_def "False ==> arbitrary == (@x. False)"
     1.8  
     1.9  
    1.10  end