renaming of theory LOmega to lomega2 in order to prevent a possible
case confusion
--- a/src/Cube/Cube.thy Thu Apr 19 13:36:07 2001 +0200
+++ b/src/Cube/Cube.thy Thu Apr 19 15:42:53 2001 +0200
@@ -1,3 +1,3 @@
-Cube = Base + L2 + Lomega + LP + LP2 + LOmega + LPomega + CC
+Cube = Base + L2 + Lomega + LP + LP2 + Lomega2 + LPomega + CC
--- a/src/Cube/IsaMakefile Thu Apr 19 13:36:07 2001 +0200
+++ b/src/Cube/IsaMakefile Thu Apr 19 15:42:53 2001 +0200
@@ -27,7 +27,7 @@
@cd $(SRC)/Pure; $(ISATOOL) make Pure
$(OUT)/Cube: $(OUT)/Pure Base.ML Base.thy CC.ML CC.thy Cube.thy L2.ML \
- L2.thy LOmega.ML LOmega.thy LP.ML LP.thy LP2.ML LP2.thy LPomega.ML \
+ L2.thy Lomega2.ML Lomega2.thy LP.ML LP.thy LP2.ML LP2.thy LPomega.ML \
LPomega.thy Lomega.ML Lomega.thy ROOT.ML
@$(ISATOOL) usedir -b $(OUT)/Pure Cube
--- a/src/Cube/LOmega.ML Thu Apr 19 13:36:07 2001 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,2 +0,0 @@
-
-val LOmega = simple @ [lam_bs,pi_bs,lam_bb,pi_bb];
--- a/src/Cube/LOmega.thy Thu Apr 19 13:36:07 2001 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,2 +0,0 @@
-
-LOmega = L2 + Lomega
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Cube/Lomega2.ML Thu Apr 19 15:42:53 2001 +0200
@@ -0,0 +1,2 @@
+
+val Lomega2 = simple @ [lam_bs,pi_bs,lam_bb,pi_bb];
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Cube/Lomega2.thy Thu Apr 19 15:42:53 2001 +0200
@@ -0,0 +1,2 @@
+
+Lomega2 = L2 + Lomega
--- a/src/Cube/ex/ex.ML Thu Apr 19 13:36:07 2001 +0200
+++ b/src/Cube/ex/ex.ML Thu Apr 19 15:42:53 2001 +0200
@@ -120,25 +120,25 @@
by (DEPTH_SOLVE (ares_tac L2 1));
uresult();
-goal LOmega.thy "|- Lam A:*.Lam B:*.Pi C:*.(A->B->C)->C : ?T";
-by (DEPTH_SOLVE (ares_tac LOmega 1));
+goal Lomega2.thy "|- Lam A:*.Lam B:*.Pi C:*.(A->B->C)->C : ?T";
+by (DEPTH_SOLVE (ares_tac Lomega2 1));
uresult();
-goal LOmega.thy "|- Lam A:*.Lam B:*.Lam x:A. Lam y:B. x : ?T";
-by (DEPTH_SOLVE (ares_tac LOmega 1));
+goal Lomega2.thy "|- Lam A:*.Lam B:*.Lam x:A. Lam y:B. x : ?T";
+by (DEPTH_SOLVE (ares_tac Lomega2 1));
uresult();
-goal LOmega.thy "A:* B:* |- ?p : (A->B) -> ((B->Pi P:*.P)->(A->Pi P:*.P))";
-by (strip_asms_tac LOmega 1);
+goal Lomega2.thy "A:* B:* |- ?p : (A->B) -> ((B->Pi P:*.P)->(A->Pi P:*.P))";
+by (strip_asms_tac Lomega2 1);
by (rtac lam_ss 1);
-by (DEPTH_SOLVE_1(ares_tac LOmega 1));
-by (DEPTH_SOLVE_1(ares_tac LOmega 2));
+by (DEPTH_SOLVE_1(ares_tac Lomega2 1));
+by (DEPTH_SOLVE_1(ares_tac Lomega2 2));
by (rtac lam_ss 1);
-by (DEPTH_SOLVE_1(ares_tac LOmega 1));
-by (DEPTH_SOLVE_1(ares_tac LOmega 2));
+by (DEPTH_SOLVE_1(ares_tac Lomega2 1));
+by (DEPTH_SOLVE_1(ares_tac Lomega2 2));
by (rtac lam_ss 1);
by (assume_tac 1);
-by (DEPTH_SOLVE_1(ares_tac LOmega 2));
+by (DEPTH_SOLVE_1(ares_tac Lomega2 2));
by (etac pi_elim 1);
by (assume_tac 1);
by (etac pi_elim 1);