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/Word/Bool_List_Representation.thy
changeset 54869 0046711700c8
parent 54863 82acc20ded73
child 54871 51612b889361 
--- a/src/HOL/Word/Bool_List_Representation.thy	Fri Dec 27 14:35:14 2013 +0100
+++ b/src/HOL/Word/Bool_List_Representation.thy	Fri Dec 27 20:35:32 2013 +0100
@@ -245,7 +245,7 @@
 
 lemma len_bin_to_bl_aux: 
   "length (bin_to_bl_aux n w bs) = n + length bs"
-  by (induct n arbitrary: w bs) auto
+  by (fact size_bin_to_bl_aux)
 
 lemma len_bin_to_bl [simp]: "length (bin_to_bl n w) = n"
   by (fact size_bin_to_bl) (* FIXME: duplicate *)
isabelle