new theorem program_equalityE
authorpaulson
Wed Nov 25 15:53:04 1998 +0100 (1998-11-25)
changeset 5969e4fe567d10e5
parent 5968 06f9dbfff032
child 5970 44ff61e1fe82
new theorem program_equalityE
src/HOL/UNITY/Traces.ML
     1.1 --- a/src/HOL/UNITY/Traces.ML	Wed Nov 25 15:52:45 1998 +0100
     1.2 +++ b/src/HOL/UNITY/Traces.ML	Wed Nov 25 15:53:04 1998 +0100
     1.3 @@ -42,6 +42,11 @@
     1.4  by (full_simp_tac (rep_ss addsimps [surjective_pairing RS sym]) 1);
     1.5  qed "program_equalityI";
     1.6  
     1.7 +val [major,minor] =
     1.8 +Goal "[| F = G; [| Init F = Init G; Acts F = Acts G |] ==> P |] ==> P";
     1.9 +by (rtac minor 1);
    1.10 +by (auto_tac (claset(), simpset() addsimps [major]));
    1.11 +qed "program_equalityE";
    1.12  
    1.13  (*** These rules allow "lazy" definition expansion ***)
    1.14