Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/HOL.thy
changeset 4371 8755cdbbf6b3
parent 4083 bcff38832d89
child 4793 03fd006fb97b 
--- 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
isabelle