1.1 --- a/src/HOL/Extraction/Warshall.thy	Mon Jun 28 15:32:17 2010 +0200
     1.2 +++ b/src/HOL/Extraction/Warshall.thy	Mon Jun 28 15:32:20 2010 +0200
     1.3 @@ -38,7 +38,7 @@
     1.4    "\<And>x. is_path' r x (ys @ [y]) z = (is_path' r x ys y \<and> r y z = T)"
     1.5    by (induct ys) simp+
     1.6  
     1.7 -theorem list_all_scoc [simp]: "list_all P (xs @ [x]) = (P x \<and> list_all P xs)"
     1.8 +theorem list_all_scoc [simp]: "list_all P (xs @ [x]) \<longleftrightarrow> P x \<and> list_all P xs"
     1.9    by (induct xs, simp+, iprover)
    1.10  
    1.11  theorem list_all_lemma: