From 3bce45dd25a714363aa21fb2338d591ffc5462b8 Mon Sep 17 00:00:00 2001
From: Gerwin Klein <gerwin.klein@data61.csiro.au>
Date: Tue, 22 Oct 2019 11:00:01 +1100
Subject: [PATCH] word_lib: avoid shadowing existing lemma

---
 lib/Word_Lib/Word_Lemmas.thy | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/lib/Word_Lib/Word_Lemmas.thy b/lib/Word_Lib/Word_Lemmas.thy
index 58a59bdc5..a09cfceb2 100644
--- a/lib/Word_Lib/Word_Lemmas.thy
+++ b/lib/Word_Lib/Word_Lemmas.thy
@@ -3710,7 +3710,7 @@ lemma le_step_down_nat:"\<lbrakk>(i::nat) \<le> n; i = n \<longrightarrow> P; i
 lemma le_step_down_int:"\<lbrakk>(i::int) \<le> n; i = n \<longrightarrow> P; i \<le> n - 1 \<longrightarrow> P\<rbrakk> \<Longrightarrow> P"
   by arith
 
-lemma mask_1[simp]: "(\<exists>x. mask x = 1)"
+lemma ex_mask_1[simp]: "(\<exists>x. mask x = 1)"
   apply (rule_tac x=1 in exI)
   apply (simp add:mask_def)
   done