| changeset 12934 | 6003b4f916c0 |
| parent 12742 | 83cd2140977d |
| child 14174 | f3cafd2929d5 |
--- a/src/HOL/NanoJava/Equivalence.thy Mon Feb 25 11:27:07 2002 +0100 +++ b/src/HOL/NanoJava/Equivalence.thy Mon Feb 25 18:02:22 2002 +0100 @@ -285,7 +285,7 @@ lemma MGF_Impl: "{} |\<turnstile> {MGT (Impl M) Z}" apply (unfold MGT_def) -apply (rule_tac 'a = state in Impl1') +apply (rule Impl1') apply (rule_tac [2] UNIV_I) apply clarsimp apply (rule hoare_ehoare.ConjI)