diff -r 4e68398cdc06 -r 4a213aaca3d9 src/Cube/cube.ML --- a/src/Cube/cube.ML Tue Dec 21 16:38:45 1993 +0100 +++ b/src/Cube/cube.ML Tue Dec 21 16:40:01 1993 +0100 @@ -10,7 +10,7 @@ val simple = [s_b,strip_s,strip_b,app,lam_ss,pi_ss]; -val L2_thy = extend_theory Cube.thy "L2" ([],[],[],[],[],None) +val L2_thy = extend_theory Cube.thy "L2" ([],[],[],[],[],[],None) [ ("pi_bs", "[| A:[]; !!x. x:A ==> B(x):* |] ==> Prod(A,B):*"), @@ -23,7 +23,7 @@ val L2 = simple @ [lam_bs,pi_bs]; -val Lomega_thy = extend_theory Cube.thy "Lomega" ([],[],[],[],[],None) +val Lomega_thy = extend_theory Cube.thy "Lomega" ([],[],[],[],[],[],None) [ ("pi_bb", "[| A:[]; !!x. x:A ==> B(x):[] |] ==> Prod(A,B):[]"), @@ -38,7 +38,7 @@ val LOmega_thy = merge_theories(L2_thy,Lomega_thy); val LOmega = simple @ [lam_bs,pi_bs,lam_bb,pi_bb]; -val LP_thy = extend_theory Cube.thy "LP" ([],[],[],[],[],None) +val LP_thy = extend_theory Cube.thy "LP" ([],[],[],[],[],[],None) [ ("pi_sb", "[| A:*; !!x. x:A ==> B(x):[] |] ==> Prod(A,B):[]"),