changeset 72792 | 26492b600d78 |
parent 72281 | beeadb35e357 |
--- a/src/HOL/Library/Type_Length.thy Mon Nov 30 17:00:35 2020 +0100 +++ b/src/HOL/Library/Type_Length.thy Mon Nov 30 17:10:49 2020 +0100 @@ -113,7 +113,7 @@ lemma two_less_eq_exp_length [simp]: \<open>2 \<le> 2 ^ LENGTH('b::len)\<close> using mult_left_mono [of 1 \<open>2 ^ (LENGTH('b::len) - 1)\<close> 2] - by (cases \<open>LENGTH('b::len)\<close>) simp_all + by (cases \<open>LENGTH('b::len)\<close>) simp_all end