--- 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")];
-