--- a/src/HOL/UNITY/Project.ML Wed Dec 22 17:16:23 1999 +0100
+++ b/src/HOL/UNITY/Project.ML Wed Dec 22 17:16:53 1999 +0100
@@ -168,6 +168,11 @@
by Auto_tac;
qed "projecting_weaken";
+Goalw [projecting_def]
+ "[| projecting C h F X' X; U'<=X' |] ==> projecting C h F U' X";
+by Auto_tac;
+qed "projecting_weaken_L";
+
Goalw [extending_def]
"[| extending v C h F YA' YA; extending v C h F YB' YB |] \
\ ==> extending v C h F (YA' Int YB') (YA Int YB)";
@@ -199,6 +204,11 @@
by Auto_tac;
qed "extending_weaken";
+Goalw [extending_def]
+ "[| extending v C h F Y' Y; Y'<=V' |] ==> extending v C h F V' Y";
+by Auto_tac;
+qed "extending_weaken_L";
+
Goal "projecting C h F X' UNIV";
by (simp_tac (simpset() addsimps [projecting_def]) 1);
qed "projecting_UNIV";