--- a/src/HOL/UNITY/Project.ML Mon Dec 13 10:54:04 1999 +0100
+++ b/src/HOL/UNITY/Project.ML Wed Dec 15 10:45:37 1999 +0100
@@ -545,6 +545,12 @@
Collect_eq_extend_set RS sym]));
qed "extend_preserves";
+Goal "inj h ==> (extend h G : preserves g)";
+by (auto_tac (claset(),
+ simpset() addsimps [preserves_def, extend_def, extend_act_def,
+ stable_def, constrains_def, g_def]));
+qed "inj_extend_preserves";
+
(** Strong precondition and postcondition; doesn't seem very useful. **)
Goal "F : X guarantees[v] Y ==> \