--- a/thys/Turing_Hoare.thy	Wed Jan 14 09:08:51 2015 +0000
+++ b/thys/Turing_Hoare.thy	Wed Dec 19 16:10:58 2018 +0100
@@ -2,7 +2,7 @@
    Author: Jian Xu, Xingyuan Zhang, and Christian Urban
 *)
 
-header {* Hoare Rules for TMs *}
+chapter {* Hoare Rules for TMs *}
 
 theory Turing_Hoare
 imports Turing
@@ -145,7 +145,8 @@
   next 
     case False
     then obtain n3 where "n = n2 - n3"
-      by (metis diff_le_self le_imp_diff_is_add nat_add_commute nat_le_linear)
+      using diff_le_self le_imp_diff_is_add nat_le_linear
+      add.commute by metis
     moreover
     with eq show "\<not> is_final (steps0 (1, l, r) (A |+| B) n)"
       by (simp add: not_is_final[where ?n1.0="n2"])