src/Cube/L2.thy

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Cube/L2.thy	Tue Jan 20 18:26:26 1998 +0100
@@ -0,0 +1,9 @@
+
+L2 = Base +
+
+rules
+  pi_bs         "[| A:[]; !!x. x:A ==> B(x):* |] ==> Prod(A,B):*"
+  lam_bs        "[| A:[]; !!x. x:A ==> f(x):B(x); !!x. x:A ==> B(x):* |]
+                   ==> Abs(A,f) : Prod(A,B)"
+
+end