# HG changeset patch
# User nipkow
# Date 796230285 -7200
# Node ID f57fb576520fe662db3d9bdb686145dd30622eac
# Parent  e61b058d58d254b86ac8247b62cabc9d28df9ddc
Modified If_def to avoid ambiguity.

diff -r e61b058d58d2 -r f57fb576520f src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Fri Mar 24 12:30:35 1995 +0100
+++ b/src/HOL/HOL.thy	Sun Mar 26 17:04:45 1995 +0200
@@ -139,7 +139,7 @@
   Let_def       "Let s f == f(s)"
   Inv_def       "Inv(f::'a=>'b)  == (% y. @x. f(x)=y)"
   o_def         "(f::'b=>'c) o g == (%(x::'a). f(g(x)))"
-  if_def   "if P then x else y == @z::'a. (P=True --> z=x) & (P=False --> z=y)"
+  if_def        "If P x y == @z::'a. (P=True --> z=x) & (P=False --> z=y)"
 
 end
 
@@ -162,4 +162,3 @@
 
 val print_ast_translation =
   map alt_ast_tr' [("! ", "*All"), ("? ", "*Ex"), ("?! ", "*Ex1")];
-