# HG changeset patch
# User paulson
# Date 987687773 -7200
# Node ID b736de4cb913f32217db5809ecd5da7aef720b65
# Parent  27f0f16f80032620bda9f81a9792bef1f6eac147
renaming of theory LOmega to lomega2 in order to prevent a possible
case confusion

diff -r 27f0f16f8003 -r b736de4cb913 src/Cube/Cube.thy
--- 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
 
diff -r 27f0f16f8003 -r b736de4cb913 src/Cube/IsaMakefile
--- 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
 
diff -r 27f0f16f8003 -r b736de4cb913 src/Cube/LOmega.ML
--- 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];
diff -r 27f0f16f8003 -r b736de4cb913 src/Cube/LOmega.thy
--- 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
diff -r 27f0f16f8003 -r b736de4cb913 src/Cube/Lomega2.ML
--- /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];
diff -r 27f0f16f8003 -r b736de4cb913 src/Cube/Lomega2.thy
--- /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
diff -r 27f0f16f8003 -r b736de4cb913 src/Cube/ex/ex.ML
--- 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);