Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned syntax
authorhaftmann
Mon, 28 Jun 2010 15:32:20 +0200
changeset 37599 b8e3400dab19
parent 37598 893dcabf0c04
child 37600 18f69eb29e66
tuned syntax
src/HOL/Extraction/Warshall.thy file | annotate | diff | comparison | revisions 
--- 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:
isabelle