src/HOL/IMP/Machines.thy
changeset 32235 8f9b8d14fc9f
parent 31970 ccaadfcf6941
child 42174 d0be2722ce9f
     1.1 --- a/src/HOL/IMP/Machines.thy	Mon Jul 27 17:36:30 2009 +0200
     1.2 +++ b/src/HOL/IMP/Machines.thy	Mon Jul 27 21:47:41 2009 +0200
     1.3 @@ -6,7 +6,7 @@
     1.4    "((x,z) \<in> R ^^ n) = (n=0 \<and> z=x \<or> (\<exists>m y. n = Suc m \<and> (x,y) \<in> R \<and> (y,z) \<in> R ^^ m))"
     1.5  apply(rule iffI)
     1.6   apply(blast elim:rel_pow_E2)
     1.7 -apply (fastsimp simp add:gr0_conv_Suc rel_pow_commute)
     1.8 +apply (auto simp: rel_pow_commute[symmetric])
     1.9  done
    1.10  
    1.11  subsection "Instructions"