adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

word_lib: avoid shadowing existing lemma

This commit is contained in:
Gerwin Klein 2019-10-22 11:00:01 +11:00 committed by Gerwin Klein
parent 0fc9ab947d
commit 3bce45dd25
1 changed files with 1 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
lib/Word_Lib/Word_Lemmas.thy
View File

@ -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