new theorem program_equalityE

--- a/src/HOL/UNITY/Traces.ML	Wed Nov 25 15:52:45 1998 +0100
+++ b/src/HOL/UNITY/Traces.ML	Wed Nov 25 15:53:04 1998 +0100
@@ -42,6 +42,11 @@
 by (full_simp_tac (rep_ss addsimps [surjective_pairing RS sym]) 1);
 qed "program_equalityI";
 
+val [major,minor] =
+Goal "[| F = G; [| Init F = Init G; Acts F = Acts G |] ==> P |] ==> P";
+by (rtac minor 1);
+by (auto_tac (claset(), simpset() addsimps [major]));
+qed "program_equalityE";
 
 (*** These rules allow "lazy" definition expansion ***)