| changeset 11507 | 4b32a46ffd29 |
| parent 11497 | 0e66e0114d9a |
| child 11508 | 168dbdaedb71 |
--- a/src/HOL/NanoJava/Equivalence.thy Wed Aug 29 21:17:24 2001 +0200 +++ b/src/HOL/NanoJava/Equivalence.thy Thu Aug 30 15:47:30 2001 +0200 @@ -249,6 +249,7 @@ apply (drule (1) eval_eval_max) apply blast +apply (simp only: split_paired_all) apply (rule hoare_ehoare.Meth) apply (rule allI) apply (drule spec, drule spec, erule hoare_ehoare.Conseq)