diff -r 893dcabf0c04 -r b8e3400dab19 src/HOL/Extraction/Warshall.thy
--- a/src/HOL/Extraction/Warshall.thy	Mon Jun 28 15:32:17 2010 +0200
+++ b/src/HOL/Extraction/Warshall.thy	Mon Jun 28 15:32:20 2010 +0200
@@ -38,7 +38,7 @@
   "\<And>x. is_path' r x (ys @ [y]) z = (is_path' r x ys y \<and> r y z = T)"
   by (induct ys) simp+
 
-theorem list_all_scoc [simp]: "list_all P (xs @ [x]) = (P x \<and> list_all P xs)"
+theorem list_all_scoc [simp]: "list_all P (xs @ [x]) \<longleftrightarrow> P x \<and> list_all P xs"
   by (induct xs, simp+, iprover)
 
 theorem list_all_lemma: