Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Quotient_Examples/Lift_DList.thy
changeset 55524 f41ef840f09d
parent 53013 3fbcfa911863
child 55565 f663fc1e653b 
--- a/src/HOL/Quotient_Examples/Lift_DList.thy	Sun Feb 16 21:33:28 2014 +0100
+++ b/src/HOL/Quotient_Examples/Lift_DList.thy	Sun Feb 16 21:33:28 2014 +0100
@@ -55,7 +55,7 @@
   {
     fix x y
     have "list_all2 cr_dlist x y \<Longrightarrow> x = List.map list_of_dlist y"
-      unfolding list_all2_def cr_dlist_def by (induction x y rule: list_induct2') auto
+      unfolding list_all2_iff cr_dlist_def by (induction x y rule: list_induct2') auto
   }
   note cr = this
   fix x :: "'a list list" and y :: "'a list list"
isabelle