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/Reversed_Bit_Lists.thy
changeset 72488 ee659bca8955
parent 72388 633d14bd1e59 
--- a/src/HOL/Word/Reversed_Bit_Lists.thy	Thu Oct 15 14:55:19 2020 +0200
+++ b/src/HOL/Word/Reversed_Bit_Lists.thy	Sat Oct 17 18:56:36 2020 +0200
@@ -1684,7 +1684,7 @@
   apply (simp add: word_split_def)
   apply transfer
   apply (cases \<open>LENGTH('b) \<le> LENGTH('a)\<close>)
-   apply (auto simp add: drop_bit_take_bit drop_bin2bl bin_to_bl_drop_bit [symmetric, of \<open>LENGTH('a)\<close> \<open>LENGTH('a) - LENGTH('b)\<close> \<open>LENGTH('b)\<close>])
+   apply (auto simp add: drop_bit_take_bit drop_bin2bl bin_to_bl_drop_bit [symmetric, of \<open>LENGTH('a)\<close> \<open>LENGTH('a) - LENGTH('b)\<close> \<open>LENGTH('b)\<close>] min_absorb2)
   done
 
 lemma word_split_bl: "std = size c - size b \<Longrightarrow>
isabelle