# HG changeset patch
# User paulson
# Date 912005584 -3600
# Node ID e4fe567d10e562957c9e93dbafd1545c9fc5c9fa
# Parent  06f9dbfff032df995ff14866dbea8b9a87c64445
new theorem program_equalityE

diff -r 06f9dbfff032 -r e4fe567d10e5 src/HOL/UNITY/Traces.ML
--- 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 ***)