changeset 1149 | 5750eba8820d |
parent 351 | 1718ce07a584 |
child 3773 | 989ef5e9d543 |
--- a/src/Cube/Cube.thy Wed Jun 21 11:35:10 1995 +0200 +++ b/src/Cube/Cube.thy Wed Jun 21 15:01:07 1995 +0200 @@ -46,8 +46,8 @@ pi_ss "[| A:*; !!x. x:A ==> B(x):* |] ==> Prod(A, B):*" - lam_ss "[| A:*; !!x. x:A ==> f(x):B(x); !!x. x:A ==> B(x):* |] \ -\ ==> Abs(A, f) : Prod(A, B)" + lam_ss "[| A:*; !!x. x:A ==> f(x):B(x); !!x. x:A ==> B(x):* |] + ==> Abs(A, f) : Prod(A, B)" beta "Abs(A, f)^a == f(a)"