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