src/HOL/Library/Type_Length.thy
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