diff -r c5cfd00e4f28 -r 6d9be46ea566 src/Cube/Lomega.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Cube/Lomega.thy	Tue Jan 20 18:26:26 1998 +0100
@@ -0,0 +1,9 @@
+
+Lomega = Base +
+
+rules
+  pi_bb         "[| A:[]; !!x. x:A ==> B(x):[] |] ==> Prod(A,B):[]"
+  lam_bb        "[| A:[]; !!x. x:A ==> f(x):B(x); !!x. x:A ==> B(x):[] |]
+                   ==> Abs(A,f) : Prod(A,B)"
+
+end