# HG changeset patch
# User eberlm <eberlm@in.tum.de>
# Date 1468578231 -7200
# Node ID 34b7e2da95f619e5142c92310db75b2fffec3fad
# Parent  0dac030afd368aa2448d8ff400a79f65b68b6183
Tuned Bool_List_Representation

diff -r 0dac030afd36 -r 34b7e2da95f6 src/HOL/Word/Bool_List_Representation.thy
--- a/src/HOL/Word/Bool_List_Representation.thy	Thu Jul 14 14:49:09 2016 +0200
+++ b/src/HOL/Word/Bool_List_Representation.thy	Fri Jul 15 12:23:51 2016 +0200
@@ -9,7 +9,7 @@
 section "Bool lists and integers"
 
 theory Bool_List_Representation
-imports Main Bits_Int
+imports Complex_Main Bits_Int
 begin
 
 definition map2 :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> 'c list"
@@ -1106,7 +1106,7 @@
   apply (case_tac m)
   apply simp
   apply (case_tac "m <= n")
-  apply auto
+   apply auto
   done
 
 lemma bin_rsplit_len: