# HG changeset patch
# User paulson
# Date 945879413 -3600
# Node ID 6c99b44b333ebafa26b80f50bf04f11a3fce7c6c
# Parent  5b95377d7538ceac9effd39b4777ae1eef941e34
new weakening laws

diff -r 5b95377d7538 -r 6c99b44b333e src/HOL/UNITY/Project.ML
--- 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";